Software Formalisms

Modern software development processes increasingly depend on complete specifications, the ability to execute the specifications expressed in a lightweight formalism, and the ability to verify properties expressed in that formalism. EDAptive Computing, Inc. (ECI) team has designed the Model Checking and Execution of Specifications using Lightweight Formalisms (ModSpec) program to deliver this combination. Our existing innovative technology building blocks will be augmented with model checking, computerized assistants, and multi-domain component libraries developed in Rosetta, a non-proprietary lightweight formal language. Specifically meeting the topic requirements this combination forms an end-to-end capability to enter or capture a technology-independent specification, evaluate it for completeness, check it for correctness, and report the results in an intuitive form. We will leverage our extensive experience with graphical systems entry, formal languages, formal methods in general, and model checking in particular. We will demonstrate the feasibility of ModSpec by extending an experimental foundation first produced under a related MDA project, or a suitable mutually agreed alternative. The Phase I result will clearly show that this powerful mix of innovative tools and mature methods will result in faster, more accurate, and more error-free software development, integration, reuse, and deployment.