Dr. Blackburn Presents Model-Based Tool Comparison at S5 Symposium
Dr. Mark Blackburn presented: Model-driven Verification and Validation at the Safe & Secure Systems & Software Symposium (S5), June 2010. He sets the stage by revisiting the challenges of costly development of software-intensive systems identified by both the DARPA META program and NASA. He provides a historical picture of the birth of the T-VEC toolsuite, and explained why the T-VEC Vector Generation System addresses some of those challenges.
Dr. Guillaume Brat (from NASA) presented: V & V of Flight-Critical Systems His talk discussed some similar issues at S5 stating that verification for DO-178B level A software is 88% of the total cost to deliver the initial system.
Dr. Kirstie Bellman presented:
Making DARPA META Goals Come True: How do we Revolutionize Verification and Validation for Complex Systems? This talk presented the DARPA challenge and goals.
Dr. Blackburn discusses some of the root causes related to the DARPA META program challenges, stating that software-intensive systems, especially those needed by DARPA, NASA, and the Air Force, require verification evidence when the requirement and design specifications use nonlinear and floating point constraints mixed with linear, logical, and bit constraints. He explains that today's formal method-based tools must provide capabilities or strategies to:
- Support analysis (theorem proving or modeling checking) to prove properties about the input specification, model or program
- Support automated test generation and associated execution that demonstrates both high fault-finding effectiveness while providing high degrees of software test code coverage
- Support verification when specifications require nonlinear, floating point constraints, in addition to linear and logical constraints across data types; this is a key difference between software and integrated circuit specifications
- Scale to large systems, where requirement and design specifications derive the verification evidence that is used in the verification of the implementation in a target system software
These are the capabilities in the T-VEC tools, and this presentation provides an explanation of these capabilities, and a tool chain comparison of other model-based testing tools.