Execution of High Level Specifications for Simulation Based Acquisition

New software development processes depend on accurate specifications; the ability to execute or animate specifications expressed in a lightweight formalism, and the ability to verify properties expressed in that formalism will greatly assist software development. EDAptive Computing, Inc. (ECI) team has designed the Animation and Execution of High Level Specifications (AniSpec) program to address this issue. AniSpec is based on the principle of using lightweight formalisms to combine intuition and formalism, specifying the system using UML Statecharts but using formal specification implemented through a System Level Design Language (SLDL) for underlying representation, understanding it via SLDL execution and animation through the Statechart, while using model checkers to prove properties of the specification correct. When using the AniSpec system, user first enters the specification into UML statecharts; then animates the specification to gain an understanding of the specification; then uses a model checker to verify properties of the specification are correct; then transfers the UML statechart specification to other UML software development tools via the XMi standard exchange mechanism. ECI will demonstrate that this is feasible by going through this process, in a limited way, as a feasibility demonstration during the Phase I effort.