Teaching MDE through the Formal Verification of Process Models

Benoit Combemale 1, * Xavier Crégut 2 Arnaud Dieumegard 2 Marc Pantel 2 Faiez Zalila 2
* Auteur correspondant
1 TRISKELL - Reliable and efficient component based software engineering
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
2 IRIT - Institut de recherche en informatique de Toulouse
Abstract : 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.
Keywords : Modeling language engineering Formal verification Metamodeling Concrete syntax specification M2M and M2T Model transformations
Type de document :
Communication dans un congrès
ECEASST. 7th Educators' Symposium @ MODELS 2011: Software Modeling in Education (EduSymp2011), Oct 2011, Wellington, New Zealand. 2011
Liste complète des métadonnées
https://hal.inria.fr/hal-00646426
Contributeur : Benoit Combemale <>
Soumis le : mardi 29 novembre 2011 - 22:58:44
Dernière modification le : mercredi 11 avril 2018 - 02:01:26
Document(s) archivé(s) le : lundi 5 décembre 2016 - 01:29:01

Fichier

edusymp2011.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00646426, version 1

Collections

INRIA | IRISA | IRISA-D4 | UNIV-TLSE3 | UNIV-TLSE2 | SMS | UR1-UFR-ISTIC | UNIV-RENNES | INRIA-RENGRE

Citation

Benoit Combemale, Xavier Crégut, Arnaud Dieumegard, Marc Pantel, Faiez Zalila. Teaching MDE through the Formal Verification of Process Models. ECEASST. 7th Educators' Symposium @ MODELS 2011: Software Modeling in Education (EduSymp2011), Oct 2011, Wellington, New Zealand. 2011. 〈hal-00646426〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

563

Téléchargements de fichiers

284

Contact


archive-ouverte@inria.fr