Abstract de la publi numéro 13425
Model Driven Engineering (MDE) and formal methods (FM) play a key
role in the development of Safety Critical Systems (SCS). They promote user oriented
abstraction and formal specification using Domain Specific Modeling Languages
(DSML), early Validation and formal Verification (V&V) using efficient
dedicated technologies and Automatic Code and Documentation Generation. Their
combined use allow to improve system qualities and reduce development costs.
However, in most computer science curriculae, both domains are usually taught
independently. MDE is associated to practical software engineering and FM to theoretical
computer science. This contribution relates a course about MDE for SCS
development that bridges the gap between these domains. It describes the content
of the course and provides the lessons learned from its teaching. It focuses on early
formal verification using model checking of a DSML for development process modeling.
MDE technologies are illustrated both on language engineering for CASE tool
development and on development process modeling. The case study also highlights
the unification power of MDE as it does not target traditional executable software.