[go: up one dir, main page]
Skip to main content

Advertisement

Springer Nature Link
Log in

VerifCar: a framework for modeling and model checking communicating autonomous vehicles

  • Published:
Autonomous Agents and Multi-Agent Systems Aims and scope Submit manuscript

Abstract

This paper presents a framework, called VerifCar, devoted to the validation of decision policies of communicating autonomous vehicles (CAVs). The approach focuses on the formal modeling of CAVs by means of timed automata, allowing a formal and exhaustive analysis of the behaviors of vehicles. VerifCar supports a parametric modeling of CAV systems as a network of timed automata tailored for verification and limiting the well-known state space explosion. As an illustration, VerifCar is applied to check robustness and efficiency, as well as to asses the impact of communication delays on the decision algorithms of CAVs, on well chosen case studies representing real-life critical situations.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. A type corresponds here to a range of integers.

  2. It only occurs for decision transitions, not for communication ones, for which actions are independent of the vehicles’ state, and therefore of the update function.

  3. Actually twice the loss of precision, thanks to rounding.

  4. The operator \(\rightarrow \), called “leads to”, supported by the UPPAAL model checker is equivalent to \(A G\ (\lnot \ before (C,A) \vee A F\ before (B,A))\).

  5. i.e., when \(\mathsf {Norm}_x = \mathsf {Gran}_ v /2\): in this example \(\mathsf {Norm}_x = 0.05\) m/s.

References

  1. Alur, R., Courcoubetis, C., & Dill, D. (1993). Model checking in dense real-time. Information and Computation, 104(1), 2–34.

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., & Dill, D. (1990). Automata for modelling real-time systems. In Proceedings of the international colloquium on automata, languages and programming (ICALP’90), volume 443 of LNCS (pp. 322–335). Springer.

  3. Alur, R., & Dill, D. (1994). A theory of timed automata. Theoretical Computer Science, 126(2), 183–235.

    Article  MathSciNet  MATH  Google Scholar 

  4. Arcile, J., Devillers, R., Klaudel, H., Klaudel, W., & Woźna-Szcześniak, B. (2018). Modeling and checking robustness of communicating autonomous vehicles. In S. Omatu, S. Rodríguez, G. Villarrubia, P. Faria, P. Sitek, & J. Prieto (Eds.), Distributed computing and artificial intelligence, 14th international conference (pp. 173–180). Berlin: Springer.

    Chapter  Google Scholar 

  5. Arcile, J., Sobieraj, J., Klaudel, H., & Hutzler, G. (2018). Combination of simulation and model-checking for the analysis of autonomous vehicles’ behaviors: A case study. In F. Belardinelli & E. Argente (Eds.), Multi-agent systems and agreement technologies. Berlin: Springer.

    Google Scholar 

  6. Bai, F., & Krishnan, H. (September, 2006). Reliability analysis of DSRC wireless communication for vehicle safety applications. In IEEE intelligent transportation systems conference (pp. 355–362).

  7. Bilstrup, K., Uhlemann, E., Strom, E. G., & Bilstrup, U. (September, 2008). Evaluation of the IEEE 802.11p MAC method for vehicle-to-vehicle communication. In IEEE vehicular technology conference (pp. 1–5).

  8. Biswas, S., Tatchikou, R., & Dion, F. (2006). Vehicle-to-vehicle wireless communication protocols for enhancing highway traffic safety. IEEE Communications Magazine, 44(1), 74–82.

    Article  Google Scholar 

  9. Blokpoel, R. J., Krajzewicz, D., & Nippold, R. (2010) Unambiguous metrics for evaluation of traffic networks. In IEEE intelligent transportation systems conference (pp. 1277–1282).

  10. Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model checking. Cambridge: MIT Press.

    Google Scholar 

  11. Devillers, R., & Klaudel, H. (2016). Abstraction strategies for computing travelling or looping durations in networks of timed automata. In M. Fränzle & N. Markey (Eds.), 14th international conference, FORMATS 2016, proceedings, volume 9884 of LNCS (pp. 140–156). Springer.

  12. Emerson, E. A. (1990). Temporal and modal logic. In J. van Leeuwen (Ed.), Handbook of theoretical computer science (Vol. b, pp. 995–1072). Cambridge, MA: MIT Press.

    Google Scholar 

  13. Foughali, M., Berthomieu, B., Dal Zilio, S., Ingrand, F., & Mallet, A. (November 2016). Model checking real-time properties on the functional layer of autonomous robots. In International conference on formal engineering methods (ICFEM 2016), Tokyo, Japan.

  14. Furda, A., & Vlacic, L. (2011). Enabling safe autonomous driving in real-world city traffic using multiple criteria decision making. IEEE Intelligent Transportation Systems Magazine, 3(1), 4–17.

    Article  Google Scholar 

  15. Glaser, S., Vanholme, B., Mammar, S., Gruyer, D., & Nouveliere, L. (2010). Maneuver-based trajectory planning for highly autonomous vehicles on real road with traffic and driver interaction. IEEE Transactions on Intelligent Transportation Systems, 11(3), 589–606.

    Article  Google Scholar 

  16. Kamali, M., Dennis, L. A., McAree, O., Fisher, M., & Veres, S. M. (2017). Formal verification of autonomous vehicle platooning. Science of Computer Programming, 148, 88–106.

    Article  Google Scholar 

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

    Article  Google Scholar 

  18. Kong, S., Gao, S., Chen, W., & Clarke, E. (2015). dreach: \(\delta \)-reachability analysis for hybrid systems. In C. Baier & C. Tinelli (Eds.), Tools and algorithms for the construction and analysis of systems (pp. 200–205). Berlin: Springer.

    Google Scholar 

  19. Kuwata, Y., Teo, J., Fiore, G., Karaman, S., Frazzoli, E., & How, J. P. (2009). Real-time motion planning with applications to autonomous urban driving. IEEE Transactions on Control Systems Technology, 17(5), 1105–1118.

    Article  Google Scholar 

  20. Levinson, J., & Thrun, S. (May 2010). Robust vehicle localization in urban environments using probabilistic maps. In IEEE international conference on robotics and automation (pp. 4372–4378).

  21. Likhachev, M., & Ferguson, D. (2009). Planning long dynamically feasible maneuvers for autonomous vehicles. The International Journal of Robotics Research, 28(8), 933–945.

    Article  Google Scholar 

  22. Minderhoud, M., & Bovy, P. (2001). Extended time-to-collision measures for road traffic safety assessment. Accident Analysis & Prevention, 33(1), 89–97.

    Article  Google Scholar 

  23. O’Kelly, M., Abbas, H., & Mangharam, R. (2016). APEX : Autonomous vehicle plan verification and execution. In SAE World Congress.

  24. Platzer, A., & Quesel, J.-D. (2009). European train control system: A case study in formal verification. In K. Breitman & A. Cavalcanti (Eds.), Formal methods and software engineering (pp. 246–265). Berlin: Springer.

    Chapter  Google Scholar 

  25. Quottrup, M. M., Bak, T., & Zamanabadi, R. I. (April, 2004). Multi-robot planning: A timed automata approach. In IEEE international conference on robotics and automation, 2004. Proceedings. ICRA ’04. 2004 (Vol. 5, pp. 4417–4422).

  26. Stanley, K. D., Sorensen, P., Samaras, C., Anderson, J. M., Kalra, N., & Oluwatola, T. A. (2016). Autonomous vehicle technology. A guide for policymakers. Research Reports. RAND Corporation. ISBN: 978-0-8330-8398-2.

  27. Treiber, M., & Kesting, A. (2013). Trajectory and floating-car data (pp. 7–12). Berlin: Springer.

    MATH  Google Scholar 

  28. Uppaal. http://www.uppaal.org/. Accessed 29 Apr 2019.

  29. Urmson, C., et al. (2008). Autonomous driving in urban environments: Boss and the urban challenge. Journal of Field Robotics, 25(8), 425–466.

    Article  Google Scholar 

  30. Vogel, K. (2003). A comparison of headway and time to collision as safety indicators. Accident Analysis & Prevention, 35(3), 427–433.

    Article  Google Scholar 

  31. Willke, T. L., Tientrakool, P., & Maxemchuk, N. F. (2009). A survey of inter-vehicle communication protocols and their applications. IEEE Communications Surveys Tutorials, 11(2), 3–20.

    Article  Google Scholar 

  32. Wooldridge, M. (2009). An introduction to multi-agent systems (2nd ed.). Hoboken: Wiley.

    Google Scholar 

  33. Zhang, S., Deng, W., Zhao, Q., Sun, H., & Litkouhi, B. (2013). Dynamic trajectory planning for vehicle autonomous driving. In IEEE international conference on systems, man, and cybernetics (pp. 4161–4166).

Download references

Author information

Authors and Affiliations

  1. IBISC, Univ Evry, Université Paris-Saclay, 91025, Évry, France

    Johan Arcile & Hanna Klaudel

  2. ULB, Brussels, Belgium

    Raymond Devillers

Authors
  1. Johan Arcile
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Raymond Devillers
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Hanna Klaudel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Johan Arcile.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Appendix: TTC Algorithm

Appendix: TTC Algorithm

Algorithm 3 formalizes the computation of the TTC value used in our experiments. \(px_i\) (respectively \(py_i\)) is the longitudinal (respectively lateral) position of vehicle i, and \( Long \) (respectively \( Lat \)) is the longitudinal (respectively lateral) gap below which there is a collision. Similarly, \(vx_i\) (respectively \(vy_i\)) is the longitudinal speed (respectively lateral speed) value of vehicle i. \( Long \) and \( Lat \) depend on each vehicle length and width: typically, as the position is centered on the vehicle, \( Long \) will be the mean of the length of the two vehicles, while \( Lat \) will be the mean of the width of the two vehicles.

figure c

This algorithm consists in computing the starting time \(X_{in}\) and the ending time \(X_{out}\) of the longitudinal time overlap (respectively \(Y_{in}\) and \(Y_{out}\) for the lateral time overlap). If no overlapping (either longitudinal or lateral) is ever going to occur, the starting time will be given the value \(\infty \) and the ending time will be set to 0. Afterwards, the computation of TTC is performed by returning the smallest value in the intersection between longitudinal and lateral time overlaps.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Arcile, J., Devillers, R. & Klaudel, H. VerifCar: a framework for modeling and model checking communicating autonomous vehicles. Auton Agent Multi-Agent Syst 33, 353–381 (2019). https://doi.org/10.1007/s10458-019-09409-x

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10458-019-09409-x

Keywords

Search

Navigation