Software Formalisms

EDAptive Computing, Inc. [ECI] team is pleased to submit this Phase II proposal in response to SBIR solicitation number MDA05-051: Software Formalisms. By its assigned mission MDA must develop some of the most complex software systems in the world under the most extreme real-time reliability and correctness constraints imaginable. These systems must work the first time and every time, yet there is very little ability to test systems under operational conditions. Costs and risks associated with the development of complex, real-time critical software must be reduced, while safety-based quality metrics are maintained and increased. In our Phase I ModSpec (Model Checking and Execution of Specifications Using Lightweight Formalisms) project we researched and developed a solution providing: integrated graphical entry of specifications, execution of those specifications to increase understanding, and mathematically-based formal verification of those specifications. The capability defined will enable development of specifications in logic that are provably correct. In Phase II, ECI and the ModSpec team will produce the full ModSpec tool and demonstrate it on existing, working MDA projects, immediately making the transition to active MDA applications.