Teaching MDE through the Formal Verification of Process Models

Benoît Combemale, Xavier Crégut, Arnaud Dieumegard, Marc Pantel and Faiez Zalila.

Abstract

Model Driven Engineering (MDE) plays a key role in the current development of Safety Critical Systems (SCS) relying on Domain Specific Modeling Languages (DSML), early Validation and Verification (V&V) and Automatic Code Generation. It allows to reduce the development cost and to improve the system qualities.

This contribution describes the content and provides the lessons learned from a course about MDE for SCS development that started five years ago. This course focuses on the use of DSML to allow early V&V based on formal methods. It relies on a case study for process modeling and verification that leads students to experiment the various MDE tools that ease the definition and implementation of Domain Specific CASE tool.

MDE is introduced as a cornerstone of the formal methods course that introduces specific formalisms (e.g., Petri net) dedicated to efficient verification tools (e.g., model-checker), and the software modeling course that promotes user oriented abstraction through DSML. The unification power of MDE is also highlighted by the case study about process modeling that does not target traditional executable software.

Slides

You can find the slides of the presentation here.