publication . Article . Other literature type . Preprint . 2017

Formal verification of autonomous vehicle platooning

Kamali, Maryam; Dennis, Louise A.; McAree, Owen; Fisher, Michael; Veres, Sandor M.;
Open Access English
  • Published: 15 Nov 2017
Abstract
Abstract The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the behaviours of the vehicles in these platoons must be certified. This is non-trivial and goes beyond current certification requirements, for human-controlled vehicles, in that these vehicles can act autonomously . In this paper, we show how formal verification can contribute to the analysis of these new, and increasingly autonomous, systems. An appropriate overall representation for vehicle platooning is as a multi-agent system in which each agent captures the “autonomous decisions” c...
Subjects
free text keywords: Agent programming, Model checking, Vehicle platooning, /dk/atira/pure/subjectarea/asjc/1700/1712, Software, Certification, Formal verification, Global system, Programming language, computer.software_genre, computer, Systems engineering, Strategy, Computer science, Computer Science - Artificial Intelligence, Computer Science - Software Engineering
Related Organizations
22 references, page 1 of 2

[1] R. Alur, C. Courcoubetis, and D. Dill. Model-Checking in Dense Real-time. Information and Computation, 104:2-34, 1993. [OpenAIRE]

[2] C. Bergenhem, Q. Huang, A. Benmimoun, and T. Robinson. Challenges of Platooning on Public Motorways. In Proc. 17th World Congress on Intelligent Transport Systems, pages 1-12, 2010.

[3] S. Colin, A. Lanoix, O. Kouchnarenko, and J. Souquières. Using CSPkb Components: Application to a Platoon of Vehicles. In Formal Methods for Industrial Critical Systems, pages 103-118. Springer, 2009. [OpenAIRE]

[4] L. A. Dennis and B. Farwer. Gwendolen: A BDI Language for Verifiable Agents. In AISB'08 Workshop on Logic and the Simulation of Interaction and Reasoning. AISB, 2008.

[5] L. A. Dennis, M. Fisher, N. K. Lincoln, A. Lisitsa, and S. M. Veres. Declarative Abstractions for Agent Based Hybrid Control Systems. In Declarative Agent Languages and Technologies VIII, volume 6619 of LNCS, pages 96-111. Springer, 2011.

[6] L. A. Dennis, M. Fisher, and M. Webster. Two-Stage Agent Program Verification. Journal of Logic and Computation, 2015. In press.

[7] L. A. Dennis, M. Fisher, M. P. Webster, and R. H. Bordini. Model Checking Agent Programming Languages. Automated Software Engineering, 19(1):5-63, 2012.

[8] M. El-Zaher, J.-M. Contet, P. Gruer, F. Gechter, and A. Koukam. Compositional Verification for Reactive Multi-Agent Systems Applied to Platoon non Collision Verification. Stud. Inform. Univ., 10(3):119-141, 2012.

[9] M. Finger and D. M. Gabbay. Combining Temporal Logic Systems. Notre Dame Journal of Formal Logic, 37(2):204-232, 1996. [OpenAIRE]

[10] M. Fisher, L. A. Dennis, and M. Webster. Verifying Autonomous Systems. ACM Communications, 56(9):84-93, 2013.

[11] D. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev. Many-Dimensional Modal Logics: Theory and Applications. Number 148 in Studies in Logic and the Foundations of Mathematics. Elsevier Science, 2003. [OpenAIRE]

[12] T. A. Henzinger. The Theory of Hybrid Automata. In Proc. 11th IEEE Symposium on Logic in Computer Science, pages 278-. IEEE Computer Society, 1996.

[13] M. Hilscher, S. Linker, and E.-R. Olderog. Proving Safety of Traffic Manoeuvres on Country Roads. In Z. Liu, J. Woodcock, and H. Zhu, editors, Theories of Programming and Formal Methods, volume 8051 of LNCS, pages 196-212. Springer, 2013.

[14] JPF. . . the Swiss Army Knife of JavaT M verification. http://babelfish. arc.nasa.gov/trac/jpf/. Accessed 26-January-2016.

[15] S. Konur, M. Fisher, and S. Schewe. Combined Model Checking for Temporal, Probabilistic, and Real-time Logics. Theoretical Computer Science, 503:61-88, 2013. [OpenAIRE]

22 references, page 1 of 2
Abstract
Abstract The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the behaviours of the vehicles in these platoons must be certified. This is non-trivial and goes beyond current certification requirements, for human-controlled vehicles, in that these vehicles can act autonomously . In this paper, we show how formal verification can contribute to the analysis of these new, and increasingly autonomous, systems. An appropriate overall representation for vehicle platooning is as a multi-agent system in which each agent captures the “autonomous decisions” c...
Subjects
free text keywords: Agent programming, Model checking, Vehicle platooning, /dk/atira/pure/subjectarea/asjc/1700/1712, Software, Certification, Formal verification, Global system, Programming language, computer.software_genre, computer, Systems engineering, Strategy, Computer science, Computer Science - Artificial Intelligence, Computer Science - Software Engineering
Related Organizations
22 references, page 1 of 2

[1] R. Alur, C. Courcoubetis, and D. Dill. Model-Checking in Dense Real-time. Information and Computation, 104:2-34, 1993. [OpenAIRE]

[2] C. Bergenhem, Q. Huang, A. Benmimoun, and T. Robinson. Challenges of Platooning on Public Motorways. In Proc. 17th World Congress on Intelligent Transport Systems, pages 1-12, 2010.

[3] S. Colin, A. Lanoix, O. Kouchnarenko, and J. Souquières. Using CSPkb Components: Application to a Platoon of Vehicles. In Formal Methods for Industrial Critical Systems, pages 103-118. Springer, 2009. [OpenAIRE]

[4] L. A. Dennis and B. Farwer. Gwendolen: A BDI Language for Verifiable Agents. In AISB'08 Workshop on Logic and the Simulation of Interaction and Reasoning. AISB, 2008.

[5] L. A. Dennis, M. Fisher, N. K. Lincoln, A. Lisitsa, and S. M. Veres. Declarative Abstractions for Agent Based Hybrid Control Systems. In Declarative Agent Languages and Technologies VIII, volume 6619 of LNCS, pages 96-111. Springer, 2011.

[6] L. A. Dennis, M. Fisher, and M. Webster. Two-Stage Agent Program Verification. Journal of Logic and Computation, 2015. In press.

[7] L. A. Dennis, M. Fisher, M. P. Webster, and R. H. Bordini. Model Checking Agent Programming Languages. Automated Software Engineering, 19(1):5-63, 2012.

[8] M. El-Zaher, J.-M. Contet, P. Gruer, F. Gechter, and A. Koukam. Compositional Verification for Reactive Multi-Agent Systems Applied to Platoon non Collision Verification. Stud. Inform. Univ., 10(3):119-141, 2012.

[9] M. Finger and D. M. Gabbay. Combining Temporal Logic Systems. Notre Dame Journal of Formal Logic, 37(2):204-232, 1996. [OpenAIRE]

[10] M. Fisher, L. A. Dennis, and M. Webster. Verifying Autonomous Systems. ACM Communications, 56(9):84-93, 2013.

[11] D. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev. Many-Dimensional Modal Logics: Theory and Applications. Number 148 in Studies in Logic and the Foundations of Mathematics. Elsevier Science, 2003. [OpenAIRE]

[12] T. A. Henzinger. The Theory of Hybrid Automata. In Proc. 11th IEEE Symposium on Logic in Computer Science, pages 278-. IEEE Computer Society, 1996.

[13] M. Hilscher, S. Linker, and E.-R. Olderog. Proving Safety of Traffic Manoeuvres on Country Roads. In Z. Liu, J. Woodcock, and H. Zhu, editors, Theories of Programming and Formal Methods, volume 8051 of LNCS, pages 196-212. Springer, 2013.

[14] JPF. . . the Swiss Army Knife of JavaT M verification. http://babelfish. arc.nasa.gov/trac/jpf/. Accessed 26-January-2016.

[15] S. Konur, M. Fisher, and S. Schewe. Combined Model Checking for Temporal, Probabilistic, and Real-time Logics. Theoretical Computer Science, 503:61-88, 2013. [OpenAIRE]

22 references, page 1 of 2
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue