A Software Hub for High Assurance Model-Driven Development and Analysis

The proposed project will develop a software hub designed to facilitate interoperability among tools for modeling and analysis of control software. The framework will rely on a general-purpose, intermediate language that will serve as the means of communication among tools. The hub will include translators from various commercial modeling notations into the hub language, as well as translators from the hub language to various analysis engines. The specific technical activities ro be undertaken during this project include the following. . Work with Kestrel Technology to define the hub language. . Implement a translator from Simulink(R)/Stateflow(R) (the most widely used modeling notation in aerospace and military applications) to the hub language. . Implement a translator from the hub language to the Salsa invariant checker developed at the Naval Research Laboratory. . Improve Salsa's support for analyzing embedded software models. . Implement a capability to import hub-language models into Reactis(R), the flagship automated-testing product of Reactive Systems, Inc.