Yann Duplouy PhD Defence

Practical information

Date and time

Monday, November 26th 2018, 14:00 CET.


Amphithéâtre Marie Curie
École Normale Supérieure Paris-Saclay
61, avenue du Président Wilson
94 230 Cachan

How to come

Have a look to this page for direction to the campus from the RER B station Bagneux, and then this map for direction on the campus. The Amphitéâtre Marie Curie is in the main building; enter the Bâtiment d'Alembert using the upper front entrance, then turn to your left and it is at the end of the corridor.


The slides (in French) that have been used for the presentation are available through this link. The example illustrated during the defence can be replayed with the files given in this compressed folder.



Applying Formal Methods to Autonomous Vehicle Control


Statistical model-checking, Autonomous Vehicle, Simulink


This thesis takes place in the conception of autonomous vehicles, and more specifically in the verification of controlers of such vehicles. Our contributions are the following : (1) give a syntax and a semantics for a hybrid systems model, (2) extend the capacities of the model-checker Cosmos to that kind of models, and (3) empirically confirm the relevance of our approach on typical study cases of autonomous vehicles.

We have decided to combine high-level stochastic Petri networks (which is the input formalism of Cosmos) with the input formalism of Simulink to obtain an adequate expressive power. Indeed, Simulink is vastly used in the automotive industry and numerous controllers have been specified using this tool. However, Simulink does not have a formally defined semantics. This lead us to design such a semantics in two steps : first, introducing an exact but not operational semantics, then completing it by an approximate semantics that includes the targeted approximation level.

In order to combine the discrete events model of Petri nets and the continous model specified in Simulink, the syntax we have proposed is an interface that relies on new transition types ; its semantics consists of an extension of the simulation loop. The evaluation of this new formalism has been entirely implemented into Cosmos.

Using this new formalism, we have designed and studied the two following study cases : on one hand, a heavy traffic on a motorway segment, and on the other hand the insertion of a vehicle into a motorway. The analysis of the corresponding modelisations has shown the relevance of our approach.


The manuscript is available through this link


DANG ThaoRapporteure
DEMONGODIN IsabelRapporteure
HÉLOUET LoïcExaminateur
KLOUL LeïlaExaminatrice
PEKERGIN NihalExaminatrice
BERARD BéatricePhD advisor
HADDAD SergePhD advisor

About LSV