Room 206 (2nd floor, badged access)
18 avril 2024 - 14h00
Formal Model-Driven Engineering
par Akram Idani de LIG (Vasco), Ensimag
Abstract: My research works are dedicated to the integration of two well known paradigms: Formal Methods (FM) and Model-Driven Engineering (MDE). I call this integration Formal MDE (FMDE). In fact, several works have been already done in order to strengthen the MDE paradigm with formal reasoning, and therefore make it more viable as far as safety and security concerns have to be addressed. When taken separately, these works provide a partial coverage of MDE, but when combined they can address a wide range of models and languages. During the last decade, I investigated two directions in which the FMDE paradigm proved its value: (i) Model-Driven Security (MDS), and (ii) Domain-Specific Languages (DSLs). Under the MDE umbrella, both the MDS and DSL communities advocate for the use of models throughout the development process, providing solutions to the validation problem (`do the right system'). Nonetheless, the verification problem (`do the system right') is still a major challenge, perhaps because formal reasoning (i.e. model-checking and/or theorem proving) was not apart of the MDE initiative. To be pragmatic my contributions build on well-established notations: mainly UML and B, and − at a smaller scale − BPMN, CSP, Z and Petri-Nets. Besides, the obtained results can be inspiring and, in my opinion, should be extended with other (semi-)formal languages, which would confer to FMDE a broader spectrum. The talk summarizes for every research direction (respectively MDS and DSLs) the challenges that guided my works, and gives an overview of my contributions in the field.
Candidat sur le poste de prof Polytech/Verimag
