System and Component Software Specification, Run-time Verification and Automatic Test Generation

The following background technology is described in Part 5: Run-time Verification (RV), White Box Automatic Test Generation (WBATG). Part 5 also describes how WBATG and RV yield Executable Model Checking (EMC). This proposal proposes using RV, WBATG and EMC for system level software verification. Similar techniques are commercially available for component level software (see Part 5 -- StateRover). The proposal suggests enhancing component-level UML-statechart visual modeling, code generation, Formal Specification of Correctness Properties (FS), RV, WBATG, and EMC towards the end of meeting the technology need of the subtopic, as follows: 1. Integrated specification-based and model-based WBATG for UML statechart models enhanced with FS. Having a seamless WBATG is required for system level verification because systems typically consist of a plurality of models and specifications making human driven verification difficult to perform. 2. Integrated white-box test generation of (1) with system level modeling using modeling. This integration will enable the use of system level data and models by the WBATG. 3. FS, RV, and WBATG's using the following system FS languages: Message Sequence Charts (MSC's) and Harel's Live Sequence Charts (LCS's). Items 1, 2 enable system level EMC as well as component-level EMC. Item 3 enables system level FS.