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

The project team will develop technology for allowing commercial modeling environments to interoperate with model-based testing and other quality assurance tools for distributed, real-time embedded systems. The proposed work will be focused on the development of an appropriate intermediate notation, called a "hub language", into which models can be translated and analysis tools targeted. The starting point of the investigation will be an intermediate language developed by the proposers for supporting the analysis of the Simulink / Stateflow, the industry-leading modeling languages for embedded control applications. The existing language will be analyzed for suitability for other commercial modeling languages, such as UML, matrixX and Esterel. Subsequently, effort needed to adapt model checkers such as the Salsa verifier to handle this notation will be studied. Specific strategies will also be developed for conveying diagnostic information explaining errors uncovered by model checkers back to the modeling language level.