Execution of High Level Specifications for Simulation Based Acquisition

We proposal new specification and lightweight verification technique based on three novel techniques invented by the PI. The first is a formal specification language named NTLCharts, which combines UML statechart diagram, temporal logic, and natural language. NTLCharts are visual, intuitive, while unambiguous and formal. The second technique consists of two lightweight, automatic, verification techniques: (i) run-time monitoring of assertions automatically generated from TLChart specifications, and (ii) automatic, scalable, model checking of NTLChart specifications with support for model checking of real-time systems. The third technique is armor-plating software with specification based exception handling. We will develop a cost effective design entry for NTLCharts using off the shelf drawing tools. We will then extend the drawing tool to support temporal logic and natural language entry, code generation, and assertion generation. A special assertion monitor will be developed to check the assertions during system test or execution. We will develop algorithms and code for automatic, scalable model checking, and will build tools support for specification based exception handling.