Execution of High Level Specifications for Simulation Based Acquisition

We will construct tools for solving the two primary problems with formal verification methods: the specification problem and the verification problem. Our Phase II tools will extend the Phase I StateRover proof-of-concept tool (currently actively used by MDBT-B within the Advanced Battle Manager (ABM) project). The Phase II StateRover tool-set will solve the specification problem by extending UML statecharts with NTLChart capabilities, i.e., temporal logic (with real-time and time-series constraints) and natural language specifications integrated with non-deterministic statecharts. The NTLCharts language combines the two prominent formal specification languages namely UML statecharts and temporal logic. In Phase I we demonstrated the applicability of TLCharts and its formal syntax and semantics. The Phase II StateRover tool-set will solve the verification problem by providing: 1. Tool for design, code generation and animation of NTLCharts specifications integrated with deterministic UML statechart models. 2. Run-time monitoring tool for (i) integrated non-deterministic statechart specifications within UML statecharts and (ii) for NTLChart specifications. 3. Run-time exception handling recovery tool based on non-deterministic statechart specifications integrated withUML statecharts. 4. White box automatic generator of intelligent tests for UML statecharts. 5. Black box automatic generator of intelligent tests based on NTLChart formal specifications.