• TTM and MetaEdit+, Modelica Integrated using Semantic Web Technologies
• Capers Jones Reports that T-VEC Method Finds More Software Defect
• The First Aircraft Institute of AVIC Chooses T-VEC for Model-Based Testing
• MetaEdit+ DSM and T-VEC integration
• T-VEC Project at Lockheed Martin Published in STSC CrossTalk
• Dr. Blackburn Presents Model-Based Tool Comparison at S5 Symposium
• Support for Arrays in TTM
• LDRA Integration Support
• T-VEC Wiki
• Vision Microsystems distributes T-VEC in China
• Fujisetstubi distributes T-VEC in Japan
• T-VEC Completes Model for Government Smart Card Interoperability Specification

• Archives

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.