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.
The exam is given in english only
The course exists in the following branches:
Course ID : WMM9MO65
You can find this course among all other courses.
Date of update September 21, 2022