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

Embedded software design for real time reactive system has become the bottleneck in the market introduction of complex products such as automobiles, airplanes, and in-dustrial control plants. In particular, functional correctness and reactive performance are increasingly difficult to ver-ify. The advent of model-based design methodologies has alleviated some of the verification-related problems by mak-ing the code-generation process flow automatically from the model description. Given the relative infancy of this ap-proach, 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 method-ology introducing a high potential of errors in the transfor-mation from one format to another and preventing formal analysis of the properties of the design. In this paper, 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.