Pragmatic integration of model-driven engineering and formal methods for safety-critical systems design

Marc Pantel

Institut de Recherche en Informatique de Toulouse
Institut Nationale Polytechnique de Toulouse

Thursday, 20 January 2011, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101


Slides from the talk [pdf]

Abstract: Model-driven engineering now plays a key role in the development of safety-critical systems. Domain Specific Modeling Languages provide the most appropriate expressiveness to the system designers as well as early validation, through model animation, and verification using static analysis and model checking. Automated model transformations then allow to combine the various validated and verified models and produce the final product without low level and error-prone development and verification activities.

Qualification of these automated model transformations is mandatory to avoid costly and inefficient verification of the final product. Qualification means that these transformations must be developed using the same constraints as the product they are involved in. Thus, the validation and verification of the transformation itself is a key point. Current industrially available qualified toolsets relies on classical validation and verification activities such as document and software proofreading, and the verious kind of testing. These activities are far from being exhaustive thus leaving potential holes in the product V&V schemes. State-of-the-art in academic software engineering advocates the use of semantics based proof of soundness. However, this brings a significant gap between the current know-how of common software engineers from the industry, and the mandatory skills for semantics-based verification.

Relying on the activities conducted in the TOPCASED, ES_PASS and GeneAuto projects, we propose several pragmatic structural approaches for the specification and verification of domain-specific modeling languages and model transformations that relies on common technologies such as MOF and OCL on the industrial side, and on the most advanced semantics-based verification on the academic side.

Dr Marc Pantel's visit to Tallinn is supported by the ETF/Egide Parrot programme.


Tarmo Uustalu
Last update 20.1.2011