Embedded systems are omnipresent. Increasing requirements in task complexity are met with increasing computational power and increasingly connected systems, both of which lead to more complex challenges in the area of software design. To address this rising complexity, we require standardized, well-established processes in software development, such as model-driven engineering (MDE). In MDE, a common technique to manage the complexity of models are refactorings - model transformations that increase model quality while preserving model behavior. To guarantee behavior preservation, it is desirable to employ formal verification - particularly for safety-critical systems, which are frequently encountered in the automotive, aviations and railway domains. In these areas, model-driven engineering is usually employed via MATLAB/Simulink.
The focus of CorMorant is the verification of model transformations with respect to behavior preservation, i.e. developing and evaulating techniques to establish formal proof of behavioral equivalence of input and output (source and target) models of model transformations. In CorMorant I and II, we have focused on model transformations for transition models with discrete values and discrete timing and on data flow models with continuous values and discrete or continuous timing. In CorMorant III, we plan an extension of our existing verification techniques for data flow models in order to support the verification of hybrid systems - models that have both elements with discrete and elements with continuous timing.
Concerning the verification of transformations for transition models, we plan to extend existing techniques with respect to expressive power and applicability. In particular, we would like to support weak bisimulation and weak simulation. In addition, we plan to develop methods applicable to transition models with signals assuming continuous values.
CorMorant III is a cooperation between the Technical University of Berlin and the Hasso Plattner Institute, which, in the context of the project, focus on data flow models (TUB) and transition models (HPI), respectively. Both views and techniques will be combined to investigate and establish applicability of developed techniques to data flow models with embedded transition models.
