, Il n'existe pas d'exécution possible où le véhicule B s'arrête et sa valeur d'accélération n'est jamais inférieure à deux fois la valeur du paramètre de décélération souhaitée b (c'est-à-dire jamais inférieur à ?6m

, Ces hypothèses donnent les requêtes CTL suivantes

, où acceleration est la valeur de l'accélération du véhicule A et on_the_road(A) est une variable booléenne, qui est vraie si le véhicule A n'a pas encore atteint la fin de la portion de route, ¬EG acceleration(A) ? ?6 ? on_the_road(A)

, La première hypothèse est facile à confirmer, mais il est plus intéressant de trouver un maximum pour ?. En utilisant le vérificateur de modèle, nous trouvons par dichotomie une valeur de

, Nous explorons donc le voisinage de cette valeur par simulation afin de l'affiner. La simulation indique une exécution avec e 1 = 2.2s, où un TTC inférieur à 1.7 s est trouvé, mais aucune à e 1 = 2.1s. Nous pouvons donc supposer que le maximum pour ? est en réalité de 2.1. La deuxième hypothèse semble être fausse. En fait, le vérificateur de modèle trouve une exécution violant cette propriété à la fois pour la limite supérieure, Nous affinons ensuite les limites supérieure et inférieure et obtenons finalement un résultat

, L'exploration de ces bornes par simulation ne montre aucun contre exemple

L. Enfin, Le processus de vérification a pris moins de 10 secondes pour chaque requête, malgré la complexité du système due à la taille des plages de variables et du grand nombre de positions dans lesquelles chacun des agents peut se trouver. Cependant, le système étudié ne présente pas un niveau de non-déterminisme particulièrement élevé, car nous avons limité le nombre d'actions possibles que le véhicule leader peut effectuer à un moment donné. Il était ainsi plus facile de vérifier la cohérence de nos résultats par rapport à notre cas d'étude. Pour cette raison, on pourrait faire valoir qu'il aurait été possible de vérifier tous les comportements possibles avec la seule simulation dans un délai relativement raisonnable, ce qui pourrait bien fonctionner dans ce cas particulier. Cependant, dans le cas de comportements plus complexes, cela ne semble pas être une méthode raisonnable. De plus, bien que le temps de vérification augmente également avec la taille et la complexité du système, il est encore possible, dans une certaine mesure, de vérifier de manière exhaustive les hypothèses de systèmes non déterministes complexes dans un délai raisonnable (quelques heures au plus), mais nous devons garder à l'esprit que, comme nous l'avons montré, la valeur de l'accélération peut être potentiellement très différente entre la vérification et la simulation

, Résumé du chapitre Ce chapitre présente une méthode combinant vérification de modèle et simulation afin de tirer profit des avantages respectifs de ces deux approches. La méthode consiste à énoncer puis affiner une hypothèse sur le comportement d'un système. L'hypothèse est soumise à une véri-Annexe A Coopération par négociation

, est ajouté dans la structure comm[id] contenant l'ensemble des variables liées aux données échangées et reçues par le véhicule id. Le tableau donne à l'indice j la dernière valeur de nego envoyée au véhicule id par le véhicule j. Si cette valeur est vraie, cela indique que j souhaite que id modifie son comportement

. Bibliographie,

J. Boulanger, Industrial use of formal methods : formal verification, 2013.

T. Tilley, R. Cole, P. Becker, and P. Eklund, A Survey of Formal Concept Analysis Support for Software Engineering Activities, pp.250-271, 2005.

E. M. Clarke, Model checking, Foundations of Software Technology and Theoretical Computer Science, pp.54-56, 1997.

E. , A. Emerson, and J. Y. Halpern, sometimes" and "not never" revisited : on branching versus linear time temporal logic, J. ACM, vol.1, issue.33, pp.151-178, 1986.

K. Vogel, A comparison of headway and time to collision as safety indicators, Accident Analysis & Prevention, vol.35, issue.3, pp.427-433, 2003.

M. Minderhoud and P. Bovy, Extended time-to-collision measures for road traffic safety assessment, Accident Analysis & Prevention, vol.33, issue.1, pp.89-97, 2001.

F. Pommereau, ZINC : a compiler for "any language"-coloured Petri nets, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01941485

J. Arcile, R. Devillers, and H. Klaudel, Verifcar : a framework for modeling and model checking communicating autonomous vehicles, Autonomous Agents and Multi-Agent Systems, vol.33, issue.3, pp.353-381, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02133680

, Uppaal

G. Kim, P. Larsen, W. Pettersson, and . Yi, Uppaal in a nutshell, International Journal on Software Tools for Technology Transfer (STTT), vol.1, issue.1-2, pp.134-152, 1997.

P. Taillandier, A. Duc, E. Vo, A. Amouroux, and . Drogoul, GAMA : A simulation platform that integrates geographical information data, agent-based modeling and multi-scale control, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol.7057, pp.242-258, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00688318

M. Treiber and A. Kesting, Microscopic calibration and validation of car-following models-a systematic approach, Procedia-Social and Behavioral Sciences, vol.80, pp.922-939, 2013.

M. Wooldridge, An introduction to multi-agent systems -Second Edition, 2009.

R. Alur and D. Dill, Automata for modelling real-time systems, Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP'90), vol.443, pp.322-335, 1990.

Y. Banu, S. S. Ekren, and . Heragu, Simulation based performance analysis of an autonomous vehicle storage and retrieval system, Simulation Modelling Practice and Theory, vol.19, pp.1640-1650, 2011.

H. Dia, An agent-based approach to modelling driver route choice behaviour under the influence of real-time information, Transportation Research Part C : Emerging Technologies, vol.10, issue.5, pp.331-349, 2002.

T. Shamir, How should an autonomous vehicle overtake a slower moving vehicle : design and analysis of an optimal trajectory, IEEE Transactions on Automatic Control, vol.49, issue.4, pp.607-610, 2004.

A. Kurt, L. John, Y. Yester, Ü. Mochizuki, and . Özgüner, Hybrid-state driver/-vehicle modelling, estimation and prediction, 13th International IEEE Conference on Intelligent Transportation Systems, pp.806-811, 2010.

F. Bai and H. Krishnan, Reliability analysis of DSRC wireless communication for vehicle safety applications, IEEE Intelligent Transportation Systems Conference, pp.355-362, 2006.

M. Treiber and A. Kesting, Trajectory and Floating-Car Data, pp.7-12, 2013.

S. Zhang, W. Deng, Q. Zhao, H. Sun, and B. Litkouhi, Dynamic trajectory planning for vehicle autonomous driving, IEEE International Conference on Systems, Man, and Cybernetics, pp.4161-4166, 2013.

C. Katrakazas, M. Quddus, W. Chen, and L. Deka, Real-time motion planning methods for autonomous on-road driving : State-of-the-art and future research directions. Transportation Research Part C : Emerging Technologies, vol.60, pp.416-442, 2015.

Y. Kuwata, J. Teo, G. Fiore, S. Karaman, E. Frazzoli et al., Real-time motion planning with applications to autonomous urban driving, IEEE Transactions on Control Systems Technology, vol.17, issue.5, pp.1105-1118, 2009.

A. Furda and L. Vlacic, Enabling safe autonomous driving in real-world city traffic using multiple criteria decision making, IEEE Intelligent Transportation Systems Magazine, vol.3, issue.1, pp.4-17, 2011.

M. Likhachev and D. Ferguson, Planning long dynamically feasible maneuvers for autonomous vehicles, The International Journal of Robotics Research, vol.28, issue.8, pp.933-945, 2009.

S. Glaser, B. Vanholme, S. Mammar, D. Gruyer, and L. Nouveliere, Maneuver-based trajectory planning for highly autonomous vehicles on real road with traffic and driver interaction, IEEE Transactions on Intelligent Transportation Systems, vol.11, issue.3, pp.589-606, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00653650

K. D. Stanley, P. Sorensen, C. Samaras, J. M. Anderson, N. Kalra et al., Autonomous Vehicle Technology. A Guide for Policymakers, Research Reports. RAND Corporation, 2016.

J. W. Van-lint, S. P. Hoogendoorn, and H. J. Van-zuylen, Accurate freeway travel time prediction with state-space neural networks under missing data, Transportation Research Part C : Emerging Technologies, vol.13, issue.5, pp.347-369, 2005.

L. Gang, H. S. Chang, and . Mahmassani, Travel time prediction and departure time adjustment behavior dynamics in a congested traffic system, Transportation Research Part B : Methodological, vol.22, issue.3, pp.217-232, 1988.

M. Foughali, B. Berthomieu, S. Zilio, F. Ingrand, and A. Mallet, Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots, International Conference on Formal Engineering Methods (ICFEM 2016), 2016.
URL : https://hal.archives-ouvertes.fr/hal-01346080

M. Kamali, L. A. Dennis, O. Mcaree, M. Fisher, and S. M. Veres, Formal verification of autonomous vehicle platooning, Special issue on Automated Verification of Critical Systems, vol.148, pp.88-106, 2015.

M. Kelly, H. Abbas, and R. Mangharam, APEX : Autonomous vehicle plan verification and execution, SAE World Congress, 2016.

S. Kong, S. Gao, W. Chen, and E. Clarke, dreach : ?-reachability analysis for hybrid systems, Tools and Algorithms for the Construction and Analysis of Systems, pp.200-205, 2015.

A. Platzer and J. Quesel, European train control system : A case study in formal verification, Formal Methods and Software Engineering, pp.246-265, 2009.

M. M. Quottrup, T. Bak, and R. I. Zamanabadi, Multi-robot planning : a timed automata approach, IEEE International Conference on Robotics and Automation, vol.5, pp.4417-4422, 2004.

E. E-allen, Temporal and modal logic, handbook of theoretical computer science (vol. b) : formal models and semantics, 1991.

S. Edelkamp, A. L. Lafuente, and S. Leue, Directed explicit model checking with hsf-spin, Proceedings of the 8th International SPIN Workshop on Model Checking of Software, SPIN '01, pp.57-79, 2001.

K. L. Mcmillan, Symbolic Model Checking, pp.25-60, 1993.

P. Godefroid, J. Van-leeuwen, G. Hartmanis, P. Goos, and . Wolper, Partial-order methods for the verification of concurrent systems : an approach to the state-explosion problem, vol.1032, 1996.

D. Peled, Combining partial order reductions with on-the-fly model-checking, Computer Aided Verification, pp.377-390, 1994.

P. Wolper and P. Godefroid, Partial-order methods for temporal verification, pp.233-246, 1993.

A. Miller, A. Donaldson, and M. Calder, Symmetry in temporal logic model checking, ACM Comput. Surv, vol.38, issue.3, 2006.

E. M. Clarke, E. A. Emerson, S. Jha, and A. P. Sistla, Symmetry reductions in model checking, Computer Aided Verification, pp.147-158, 1998.

G. Bhat, R. Cleaveland, and O. Grumberg, Efficient on-the-fly model checking for ctl, Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pp.388-397, 1995.

I. Beer, S. Ben-david, and A. Landver, On-the-fly model checking of rctl formulas, Computer Aided Verification, pp.184-194, 1998.

D. Peled, Combining partial order reductions with on-the-fly model-checking, Computer Aided Verification, pp.377-390, 1994.

V. Gyuris and A. Sistla, On-the-fly model checking under fairness that exploits symmetry, Computer Aided Verification, pp.232-243, 1997.

. Bryant, Graph-based algorithms for boolean function manipulation, IEEE Transactions on Computers, C, vol.35, issue.8, pp.677-691, 1986.

J. R. Burch, E. M. Clarke, K. L. Mcmillan, D. L. Dill, and L. J. Hwang, Symbolic model checking : 1020 states and beyond. Information and Computation, vol.98, pp.142-170, 1992.

N. Amla, X. Du, A. Kuehlmann, R. P. Kurshan, and K. L. Mc-millan, An analysis of sat-based model checking techniques in an industrial environment, Correct Hardware Design and Verification Methods, pp.254-268, 2005.

A. R. Bradley, Sat-based model checking without unrolling, Verification, Model Checking, and Abstract Interpretation, pp.70-87, 2011.

E. Clarke, A. Biere, R. Raimi, and Y. Zhu, Bounded model checking using satisfiability solving, Formal Methods in System Design, vol.19, issue.1, pp.7-34, 2001.

A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, Bounded model checking, Advances in computers, vol.58, issue.11, pp.117-148, 2003.

M. Sorea, Bounded model checking for timed automata, Electronic Notes in Theoretical Computer Science, vol.68, issue.5, pp.116-134, 2003.

K. L. Mcmillan, Applications of craig interpolants in model checking, Tools and Algorithms for the Construction and Analysis of Systems, pp.1-12, 2005.

N. Eén and N. Sörensson, Temporal induction by incremental sat solving. Electronic Notes in Theoretical Computer Science, vol.89, pp.543-560, 2003.

J. A. Bergstra and J. W. Klop, Process algebra for synchronous communication. Information and Control, vol.60, pp.109-137, 1984.

C. M. Jos and . Baeten, Applications of process algebra, vol.17, 2004.

X. Nicollin and J. Sifakis, An overview and synthesis on timed process algebras, Computer Aided Verification, pp.376-398, 1992.

R. Alur, C. Courcoubetis, and D. Dill, Model checking in dense real-time, Information and Computation, vol.104, issue.1, pp.2-34, 1993.

G. Behrmann, A. David, and K. G. Larsen, A Tutorial on Uppaal, pp.200-236, 2004.

J. L. Peterson, Petri Net Theory and the Modelling of Systems, 1981.

K. Jensen, Coloured Petri Nets -Basic Concepts, Analysis Methods and Practical Use, vol.1, 1992.

C. Ghezzi, D. Mandrioli, S. Morasca, and M. Pezze, A unified high-level petri net formalism for time-critical systems, IEEE Transactions on Software Engineering, vol.17, issue.2, pp.160-172, 1991.

T. L. Willke, P. Tientrakool, and N. F. Maxemchuk, A survey of inter-vehicle communication protocols and their applications, IEEE Communications Surveys Tutorials, vol.11, issue.2, pp.3-20, 2009.

S. Biswas, R. Tatchikou, and F. Dion, Vehicle-to-vehicle wireless communication protocols for enhancing highway traffic safety, IEEE Communications Magazine, vol.44, issue.1, pp.74-82, 2006.

K. Bilstrup, E. Uhlemann, E. G. Strom, and U. Bilstrup, Evaluation of the ieee 802.11p mac method for vehicle-to-vehicle communication, IEEE Vehicular Technology Conference, pp.1-5, 2008.

C. Urmson, Journal of Field Robotics Special Issue on the 2007 DARPA Urban Challenge, Part I, vol.25, pp.425-466, 2008.

J. Levinson and S. Thrun, Robust vehicle localization in urban environments using probabilistic maps, IEEE International Conference on Robotics and Automation, pp.4372-4378, 2010.

. Akers, Binary decision diagrams, IEEE Transactions on Computers, C, vol.27, issue.6, pp.509-516, 1978.

R. Alur and D. Dill, A theory of timed automata, Theoretical computer science, vol.126, issue.2, pp.183-235, 1994.

R. J. Blokpoel, D. Krajzewicz, and R. Nippold, Unambiguous metrics for evaluation of traffic networks, IEEE Intelligent Transportation Systems Conference, pp.1277-1282, 2010.

, Source templates of the verifcar framework

, Source of the mapts models and exploration algorithms, pp.2019-2029

P. G. Gipps, A behavioural car-following model for computer simulation, Transportation Research Part B, vol.15, issue.2, pp.105-111, 1981.

S. Zhang, W. Deng, Q. Zhao, H. Sun, and B. Litkouhi, Dynamic trajectory planning for vehicle autonomous driving, Proceedings -2013 IEEE International Conference on Systems, Man, and Cybernetics, SMC 2013, pp.4161-4166, 2013.

F. Bai and H. Krishnan, Reliability Analysis of DSRC Wireless Communication for Vehicle Safety Applications, IEEE Intelligent Transportation Systems Conference (ITSC), pp.355-362, 2006.

A. Kesting, M. Treiber, and D. Helbing, General Lane-Changing Model MOBIL for Car-Following Models, Transportation Research Record : Journal of Transportation Research Board, issue.1, pp.86-94, 1999.

J. Ferber and G. Weiss, Multi-agent systems : an introduction to distributed artificial intelligence, vol.1, 1999.

J. Sobieraj, Methods and tools for the design of Cooperative Intelligent Transportation Systems. Theses, Université Paris-Saclay, November, 2018.
URL : https://hal.archives-ouvertes.fr/tel-02042591

J. Arcile, R. R. Devillers, H. Klaudel, W. Klaudel, and B. Wozna-szczesniak, Modeling and checking robustness of communicating autonomous vehicles, Distributed Computing and Artificial Intelligence, 14th International Conference, pp.173-180, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01567627

J. Arcile, J. Sobieraj, H. Klaudel, and G. Hutzler, Combination of simulation and modelchecking for the analysis of autonomous vehicles' behaviors : a case study, Multi-Agent Systems and Agreement Technologies, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01918518

A. Sali, Etude de la robustesse du modèle décisionnel des véhicules autonomes et connectés en présence de redondances d'informations. Mémoire de stage de master, 2019.