Ensimag Rubrique Formation 2022

Advanced Software Modeling and Engineering - WMM9MO65

  • Number of hours

    • Lectures 36.0
    • Projects -
    • Tutorials -
    • Internship -
    • Laboratory works -
    • Written tests -


    ECTS 6.0


Be able to (quickly) develop and instrument domain specific tools that can be used by end-users to design, verify and generate the application code from high level modeling notations.




This course addresses two important and complementary perspectives in software engineering: Model-Driven Engineering and Verification/Validation. The course is built on several labs showing by practice the underlying concepts and techniques.

1) Model-Driven Engineering (MDE): MDE is an iterative development technique that allows developers to master the software complexity by applying step-by-step refinements (or integrations) of models. The development process is therefore seen as a gradual transformation of a Platform Independent Model (PIM), which specifies a business solution independently of the target technologies, to a Platform Specific Model (PSM) describing how this solution can be implemented. The course presents various well-known MDE techniques and tools:
Xtext: a mature framework used in research and industry by companies such as Oracle, Google, BMW and many more. It allows the development of domain-specific (modeling/programming) languages (called DSL). This part shows how to develop your own full DSL infrastructure, including parsers, type-checkers, as well as editors.
UML-RT: a domain-specific modeling language targeting reactive (possibly embedded) systems. This part shows how a complete executable software implementation can be produced from high-level graphical representations and is illustrated on robotic examples.
Coccinelle: a program matching and transformation engine which provides a language for modeling code patterns and specifying the underlying transformations and/or refactoring. This part shows interesting techniques for software evolution, bug correction and will be illustrated by lab sessions.

2) Verification and Validation(V&V): V&V activities are fundamental in software engineering and can be addressed through a wide range of approaches and techniques. The course shows how to ensure the correctness of the models and the resulting software using the formal B-Method, a well-known method in industry that is supported by several tools, and used by companies such as Siemens Transportation, Alstom, Thales, etc. The course focuses on the practical side of a formal method by using ProB, a powerful and user-friendly animator, constraint solver and model checker of the B-Method. thanks to its numerous capabilities, you will be able to debug a formal specification and verify its correctness. This part of the course shows also two applications of the B-Method that are related to MDE:
B for modeling secure Information Systems: we show you how to design, using UML and SecureUML, databases and access control policies and how to generate various B specifications in order to provide a way to analyse security features and also to check for malicious scenarios such as insider attacks.
B for defining correct DSLs: we show you how to embed the formal B method within MDE tools in order to provide an error-free domain-specific tool. A lab session is planned to develop a DSL tool for producer consumer robots and verify their correctness.


UML, Java, and be familiar with the first order predicate logic.


    • MCC en présentiel **
      N1 = 1/4 CC + 3/4 examen écrit
      N2 = examen écrit
    • MCC en distanciel **
      N1 = 1/4 CC + 3/4 devoir à la maison
      N2 = devoir à la maison

The exam is given in english only FR


The course exists in the following branches:

  • Curriculum - Master in Computer Science - Semester 9 (this course is given in english only EN)
see the course schedule for 2022-2023

Additional Information

Course ID : WMM9MO65
Course language(s): FR

You can find this course among all other courses.