Correct Model Transformations III (CorMorant III)

• Applicants: Professor Dr. Holger Giese; Professorin Dr. Sabine Glesner
• Subject Area: Software Engineering and Programming Languages
• Term: from 2009 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 148420506

Embedded systems are omnipresent. There is a high and even increasing complexity in the software development of embedded systems, which is a major challenge. Refactoring is a well-known approach to reduce this complexity and to make the models compliant with standards. Especially in safety-critical environments, this is important. Also, in safety-critical areas, formal verification plays a central rôle. The key property in a refactoring that needs to be guaranteed and eventually formally verified is behavioral equivalence of source and target model. The DFG project CorMorant targets the development of verification methods that can be used for proving behavioral equivalence of graph-based source and target models. In CorMorant I and II, we have already examined graph-based models whose semantics is equipped with a logical notion of time. Moreover, in CorMorant II, we have started investigations into transformations of models with a metric notion of time. These works shall now be continued in CorMorant III. To this end, we want to develop verification techniques for purely time-discrete and time-continuous data-flow models. After that, both paradigms shall be combined to obtain a theory for time-hybrid data-flow oriented models. On top of that, we aim for a notion of compositionality for hybrid data-flow models. Furthermore, we plan to develop a method that automatically proposes refactorings that are behaviorally equivalent. To also stay on the practical side, we want to enable the use of Matlab/Simulink, which is the de facto standard in the automotive, aerospace and railway industry. All these works concerning the verification of transformations of data flow models shall be continued by TUB. Moreover, we plan to combine the theory of time-hybrid models with techniques already developed in CorMorant I and II that took transformations with a logical notion of time into account. Here, the goal is to be able to prove behavioral equivalence for models that contain data-flow as well as state-oriented parts. To also demonstrate the industrial applicability, the developed methods shall be applicable to Simulink (regarding the data-flow part) as well as to Stateflow (regarding the state-oriented part). TUB and HPI will work together on this part.

• DFG Programme: Research Grants