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

The use of model-based languages for the development of embedded and distributed systems, in connection with the development of analysis tools, each with their own modeling language gives rise to two challenges. The first is how to integrate these tools in such a way that an engineer can develop a model in one language and then analyze it for a property of interest with a tool in a different language. The second challenge is to generate high-quality code from models and eliminate the error-prone and expensive task of transcribing models into code by hand. The solution to both of these problems can be accomplished with tools we call generators. Constructing individual generators to connect all the different tools and languages is not feasible. There are many combinations and each generator is a sophisticated application. Moreover, for safety critical embedded systems, it is crucial that generators be high assurance. As outlined in the solicitation, a better approach is to define a common intermediate or "hub" language and build a family of translators to and from the common language. Our SW Metro project will develop a semantically precise hub language and technology for synthesizing provably correct translators to and from the hub.