Combination of Simulation and Model-Checking for the Analysis of Autonomous Vehicles’ Behaviors: A Case Study

  • Johan ArcileEmail author
  • Jérémy SobierajEmail author
  • Hanna Klaudel
  • Guillaume Hutzler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10767)


Autonomous vehicles’ behavioural analysis represents a major challenge in the automotive world. In order to ensure safety and fluidity of driving, various methods are available, in particular, simulation and formal verification. The analysis, however, has to cope with very complex environments depending on many parameters evolving in real time. In this context, none of the aforementioned approaches is fully satisfactory, which lead us to propose a combined methodology in order to point out suspicious behaviours more efficiently. We illustrate this approach by studying a non deterministic scenario involving a vehicle, which has to react to some perilous situation.


Autonomous vehicles Simulation Verification 


  1. 1.
    Ekren, B.Y., Heragu, S.S.: Simulation based performance analysis of an autonomous vehicle storage and retrieval system. Simul. Model. Pract. Theor. 19(7), 1640–1650 (2011)CrossRefGoogle Scholar
  2. 2.
    Dia, H.: An agent-based approach to modelling driver route choice behaviour under the influence of real-time information. Transp. Res. Part C: Emerg. Technol. 10(5), 331–349 (2002)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Shamir, T.: How should an autonomous vehicle overtake a slower moving vehicle: design and analysis of an optimal trajectory. IEEE Trans. Automat. Control 49, 607–610 (2004)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Hybrid-state driver/vehicle modelling, estimation and prediction. In: 13th International IEEE Conference on Intelligent Transportation Systems, pp. 806–811 (2010)Google Scholar
  5. 5.
    Vogel, K.: A comparison of headway and time to collision as safety indicators. Accid. Anal. Prev. 35(3), 427–433 (2003)CrossRefGoogle Scholar
  6. 6.
    Minderhoud, M.M., Bovy, P.H.: Extended time-to-collision measures for road traffic safety assessment. Accid. Anal. Prev. 33(1), 89–97 (2001)CrossRefGoogle Scholar
  7. 7.
    van Lint, J., Hoogendoorn, S., van Zuylen, H.: Accurate freeway travel time prediction with state-space neural networks under missing data. Transp. Res. Part C: Emerg. Technol. 13(5), 347–369 (2005)CrossRefGoogle Scholar
  8. 8.
    Chang, G.-L., Mahmassani, H.S.: Travel time prediction and departure time adjustment behavior dynamics in a congested traffic system. Transp. Res. Part C: Emerg. Technol. 22(3), 217–232 (1988)CrossRefGoogle Scholar
  9. 9.
    Gipps, P.G.: A behavioural car-following model for computer simulation. Transp. Res. Part B 15(2), 105–111 (1981)CrossRefGoogle Scholar
  10. 10.
    Treiber, M., Kesting, A.: Elementary car-following models. In: Treiber, M., Kesting, A. (eds.) Traffic Flow Dynamics. Springer, Heidelberg (2013). Scholar
  11. 11.
    Zhang, S., Deng, W., Zhao, Q., Sun, H., Litkouhi, B.: Dynamic trajectory planning for vehicle autonomous driving. In: Proceedings - 2013 IEEE International Conference on Systems, Man, and Cybernetics, SMC 2013, pp. 4161–4166 (2013)Google Scholar
  12. 12.
    Bai, F., Krishnan, H.: Reliability analysis of DSRC wireless communication for vehicle safety applications. In: IEEE Intelligent Transportation Systems Conference (ITSC), pp. 355–362 (2006)Google Scholar
  13. 13.
    Treiber, M., Kesting, A.: Traffic Flow Dynamics. Springer, Heidelberg (2013). Scholar
  14. 14.
    Kesting, A., Treiber, M., Helbing, D.: General lane-changing model MOBIL for car-following models. Transp. Res. Rec.: J. Transp. Res. Board 1999(1), 86–94 (2007)CrossRefGoogle Scholar
  15. 15.
    Ferber, J.: Multi-Agent Systems: An Introduction to Distributed Artificial Intelligence, vol. 222. Addison-Wesley, Boston (1999)Google Scholar
  16. 16.
    Taillandier, P., Vo, D.-A., Amouroux, E., Drogoul, A.: GAMA: a simulation platform that integrates geographical information data, agent-based modeling and multi-scale control. In: Desai, N., Liu, A., Winikoff, M. (eds.) PRIMA 2010. LNCS (LNAI), vol. 7057, pp. 242–258. Springer, Heidelberg (2012). Scholar
  17. 17.
    Arcile, J., Devillers, R., Klaudel, H., Klaudel, W., Woźna-Szcześniak, B.: Modeling and checking robustness of communicating autonomous vehicles. Distributed Computing and Artificial Intelligence, 14th International Conference. AISC, vol. 620, pp. 173–180. Springer, Cham (2018). Scholar
  18. 18.
  19. 19.
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer (STTT) 1, 134–152 (1997)CrossRefGoogle Scholar
  20. 20.
    Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 1(33), 151–178 (1986)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.IBISC, Univ Evry, University of Paris-SaclayEvryFrance

Personalised recommendations