Design, formal modeling and verification of a real-time system of cooperative agents : application to communicating autonomous vehicles

Cette thèse est motivée par la question de la validation de propriétés dans un système composé de plusieurs agents mobiles prenants individuellement des décisions en temps réel.Chaque agent a une perception de l'environnement qui lui est propre et peut communiquer avec les autres agents à proximité.L'application qui a été choisie comme cas d'étude est celle des véhicules autonomes, qui du fait du large nombre de variables impliquées dans la représentation de tels systèmes, rend impossible des approches naïves.Les problématiques traitées concernent, d'une part, la modélisation d'un tel système, notamment le choix du formalisme et du niveau d'abstraction du modèle, et d'autre part, la mise en place d'un protocole d'évaluation de la prise de décision des véhicules.Ce dernier point inclut la question de l'efficacité de l'exploration de l'espace d'états du modèle.La thèse présente un ensemble de travaux, pouvant être complémentaires, visant à traiter ces problématiques.Tout d'abord, le système, composé des véhicules autonomes et de leur environnement, est défini avec précision.Il permet notamment d'observer l'impact des communications entre véhicules sur leur comportement.Le cadre logiciel VerifCar dédié à l'analyse de prise de décision de véhicules autonomes communicants est ensuite présenté.Il inclut un modèle paramétrique d'automates temporisés offrant la possibilité de vérifier des propriétés de logique temporelle.Une méthodologie d'analyse utilisant ces propriétés est présentée.On propose également une approche complémentaire permettant dans certains cas une meilleure efficacité et une plus grande expressivité.Elle est fondée sur le formalisme des MAPTs (Multi-Agent with timed Periodic Tasks), qui a été conçu pour la modélisation de systèmes temps réel d'agents coopératifs.Des algorithmes permettant une exploration dynamique des états de ce type de modèles (c'est à dire sans que l'espace d'états ne doive être préalablement construit) sont présentés.Enfin, une méthode combinée alliant la simulation aux outils de vérification de modèle afin de contrôler le niveau de réalisme est décrite et appliquée au cas d'étude.This thesis is motivated by the question of the validation of properties in a system composed of several mobile agents individually making decisions in real time.Each agent has a perception of their own environment and can communicate with other agents nearby.The application that has been chosen as a case study is that of autonomous vehicles, which because of the large number of variables involved in the representation of such systems, makes naive approaches impossible.The issues addressed concern, on the one hand, the modeling of such a system, in particular the choice of the formalism and the level of abstraction of the model, and on the other hand, the implementation of an evaluation protocol of decision making of vehicles.This last point includes the question of the efficiency of the exploration of the state space of the model.The thesis presents a set of works, which can be complementary, aiming to treat these problems.First, the system, consisting of autonomous vehicles and their environment, is precisely defined.It allows in particular to observe the impact of communications between vehicles on their behavior.The VerifCar software framework dedicated to decision-making analysis of communicating autonomous vehicles is then presented.It includes a parametric model of timed automata with the ability to check temporal logic properties.An analysis methodology using these properties is presented.A complementary approach is also proposed, which in some cases allows for greater efficiency and greater expressiveness.It is based on the formalism of MAPTs (Multi-Agent with Timed Periodic Tasks), which was designed for modeling real-time systems of cooperative agents.Algorithms allowing a dynamic exploration of the states of this type of model (that is to say without the state space having to be built beforehand) are presented.Finally, a combined method combining simulation and model verification tools to control the level of realism is described and applied to the case study