Julien De Antoni, Associate professor@Polytech’Nice and researcher@I3S/INRIA KAIROS team

The complexity of modern systems implies a development process involvingdifferent stakeholders. These stakeholders are usually using Domain Specific Languages, tailored both syntactically and semantically to their needs.

In order to embrace such development process, we proposed to make explicit the operational semantics of DSLs as well as the semantics of their interactions. More precisely we developped formal meta languages
from which the synthesis of an interpreter, a model checker and a compiler is automatic.

The talk will present some of the challenges towards formal system engineering and the (partial) solution we proposed. It will also present a small demo on the GEMOC studio, an open source software platform hosted by the Eclipse consortium to foster research on (heterogeneous) Language Engineering.

Hana Mkaouar, Post-doc at TELECOM ParisTech/LTCI, team ACES

The verification of real-time systems is a complex and delicate task, especially when they are used in safety-critical domains.  In this context , the formal methods have become one of the advocated techniques in safety-critical software engineering. Yet, they are applied on specific formalisms such as Petri nets and process algebras, based on formal semantics, to be analyzed by dedicated tools. Indeed, the formal verification techniques can not be directly applied on design languages (such as AADL), since they lack of formal semantics. For this reason, a common approach is to transform design models into formal specifications to be verified by analysis tools. In this thesis, we aim at integrating the formal methods in an AADL model-based development process. To do this, we provide a mapping of the AADL model into a formal model. Indeed, we have defined and implemented a model transformation, in order to allow the model-checking of a set of structural and behavioral properties of real-time systems.