Skip to Main content Skip to Navigation

Conception, modélisation et vérification formelle d’un système temps-réel d’agents coopératifs : application aux véhicules autonomes communicants

Abstract : This thesis is motivated by the questionof the validation of properties in a system composedof several mobile agents individually makingdecisions in real time. Each agent has a perceptionof their own environment and can communicate withother agents nearby. The application that has beenchosen as a case study is that of autonomous vehicles,which because of the large number of variables involvedin the representation of such systems, makesnaive approaches impossible. The issues addressedconcern, on the one hand, the modeling of such asystem, in particular the choice of the formalism andthe level of abstraction of the model, and on the otherhand, the implementation of an evaluation protocol ofdecision making of vehicles. This last point includesthe question of the efficiency of the exploration of thestate space of the model. The thesis presents a set ofworks, which can be complementary, aiming to treatthese problems. First, the system, consisting of autonomousvehicles and their environment, is preciselydefined. It allows in particular to observe the impactof communications between vehicles on their behavior.The VerifCar software framework dedicated todecision-making analysis of communicating autonomousvehicles is then presented. It includes a parametricmodel of timed automata with the ability tocheck temporal logic properties. An analysis methodologyusing these properties is presented. A complementaryapproach is also proposed, which in somecases allows for greater efficiency and greater expressiveness.It is based on the formalism of MAPTs(Multi-Agent with timed Periodic Tasks), which wasdesigned for modeling real-time systems of cooperativeagents. Algorithms allowing a dynamic explorationof the states of this type of model (that is tosay without the state space having to be built beforehand)are presented. Finally, a combined methodcombining simulation and model verification tools tocontrol the level of realism is described and appliedto the case study.
Complete list of metadatas

Cited literature [93 references]  Display  Hide  Download
Contributor : Frédéric Davesne <>
Submitted on : Sunday, February 16, 2020 - 8:25:38 PM
Last modification on : Monday, July 6, 2020 - 2:18:37 PM
Long-term archiving on: : Sunday, May 17, 2020 - 12:52:44 PM


Files produced by the author(s)


  • HAL Id : tel-02480653, version 1


Johan Arcile,. Conception, modélisation et vérification formelle d’un système temps-réel d’agents coopératifs : application aux véhicules autonomes communicants. Calcul formel [cs.SC]. Université Paris-Saclay, Université d'Evry Val-d'Essonne, 2019. Français. ⟨NNT : 2019SACLE029⟩. ⟨tel-02480653⟩



Record views


Files downloads