Correct-by-Construction Transformations across Design Environments for Model-Based Embedded Software Development

Embedded software design for real time reactive systems has become the bottleneck in their market introduction into complex products such as automobiles, airplanes, and industrial control plant. In particular, functional correctness and reactive performance are increasingly difficult to verify. The advent of model-based design methodologies has alleviated some of the verification-related problems by making the code-generation process flow automatically from the model description. Given the relative infancy of this approach, several companies rely upon design flows based on different tools connected together by file transfer. This way of integrating tools defeats the very purpose of the methodology, introducing a high potential of errors in the transformation from one format to another and preventing formal analysis of the properties of the design. We propose to adopt a formal transformation across different tools and we give an example of this approach by linking two tools that are widely used in the automotive domain, Simulink and ASCET. We believe that this approach can be applied to any embedded software design flow to leverage the power of all the tools in the flow.