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

This proposal is for the creation of a system-level software specification and verification tool. This proposal suggests a major leap-forward in usability of modeling, code generation, Runtime Verification (RV), and Automatic Test Generation (ATG) from the component-level to the system-level. 1. We will create a specification and run-time verification environment for system-level specifications using J-MSC assertions and distributed assertions. J-MSC assertions are a UML-based system-level formal specification language. In phase-I we demonstrated J-MSC assertion and distributed assertion specification and monitoring. In phase-II we will construct an editor, code-generator, and run-time monitor for J-MSC assertions and for distributed assertions. 2. We will create system-level verification environment, compliant with the de-facto JUnit testing framework, including: • RV of J-MSC assertions for system verification combined with statechart-assertions for the component level. • RV of distributed assertions. • System-level white-box ATG of UML controller models and assertions: white-box ATG for a plurality controller modules and for a plurality of controller instances. • Combined black-box/Matlab and white-box ATG, with support for both open-loop and closed loop techniques. • White-box ATG based on real-time contracts of system components. More »