Séminaire Systèmes embarqués critiques

Le jeudi 7 mars 2019 à Télécom Paris / Barrault. Séminaire entièrement en anglais.
March 7th 2019 at 10 a.m. in room B603.

The presentations will be given by Julien De Antoni, and Hana Mkaouar. You can find the detailed program with abstracts below.

10h00 – 10h45 : Presentation of Julien De Antoni
10h45 – 11h00 : Coffee break
11h00 – 11h45 : Presentation of Hana Mkaouar.

Towards Formal System Engineering

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.

A Formal Approach for Real-time Systems 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.