Advanced software modeling and engineering - WMM9MO65

Objectif(s)

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.

Contenu(s)

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.