Abstract
Increasing demands on safety and energy efficiency will require higher levels of automation in transportation systems. This involves dealing with safety-critical distributed coordination. In this paper we demonstrate how a Satisfiability Modulo Theories (SMT) solver can be used to prove correctness of a vehicular coordination problem. We formalise a recent distributed coordination protocol and validate our approach using an intersection collision avoidance (ICA) case study. The system model captures continuous time and space, and an unbounded number of vehicles and messages. The safety of the case study is automatically verified using the Z3 theorem prover.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Althoff, M., Althoff, D., Wollherr, D., Buss, M.: Safety verification of autonomous vehicles for coordinated evasive maneuvers. In: IEEE Intelligent Vehicles Symposium, IV (2010), doi:10.1109/IVS.2010.5548121
Alur, R.: Formal verification of hybrid systems. In: Proceedings of the Ninth ACM International Conference on Embedded Software, EMSOFT. ACM (2011), doi:10.1145/2038642.2038685
Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010), http://www.SMT-LIB.org
Bhandal, C., Bouroche, M., Hughes, A.: A process algebraic description of a temporal wireless network protocol. In: Proceedings of the Fourth International Workshop on Formal Methods for Interactive Systems (2011)
Bouroche, M.: Real-Time Coordination of Mobile Autonomous Entities. PhD thesis, Dept. of Computer Science, Trinity College Dublin (2007)
Chandra, T.D., Hadzilacos, V., Toueg, S., Charron-Bost, B.: On the impossibility of group membership. In: Fifteenth Annual ACM Symposium on Principles of Distributed Computing (PODC). ACM Press (1996), doi:10.1145/248052.248120
Damm, W., Hungar, H., Olderog, E.-R.: Verification of cooperating traffic agents. International Journal of Control 79(5) (2006), doi:10.1080/00207170600587531
De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54 (2011), doi: http://doi.acm.org/10.1145/1995376.1995394
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Dresner, K., Stone, P.: A multiagent approach to autonomous intersection management. J. Artif. Int. Res. 31(1), 591–656 (2008)
European Commission. Eu energy and transport in figures (2010), http://ec.europa.eu/energy/publications/statistics/statistics_en.htm (accessed January 2012)
Henzinger, T.: The theory of hybrid automata. In: Proceedings. Eleventh Annual IEEE Symposium on Logics in Computer Science, LICS 1966 (1996), doi:10.1109/LICS.1996.561342
Herde, C., Eggers, A., Franzle, M., Teige, T.: Analysis of hybrid systems using hysat. In: Third International Conference on Systems, ICONS (2008), doi:10.1109/ICONS.2008.17
Huang, J., Blech, J., Raabe, A., Buckl, C., Knoll, A.: Static scheduling of a time-triggered network-on-chip based on SMT solving. In: Design, Automation Test in Europe Conference Exhibition (DATE), pp. 509–514 (2012)
Livadas, C., Lygeros, J., Lynch, N.: High-level modeling and analysis of the traffic alert and collision avoidance system (tcas). Proceedings of the IEEE 88(7) (2000), doi:10.1109/5.871302
Loos, S., Platzer, A., Nistor, L.: Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 42–56. Springer, Heidelberg (2011)
Loos, S.M., Platzer, A.: Safe intersections: At the crossing of hybrid systems and verification. In: 14th International IEEE Conference on Intelligent Transportation Systems, ITSC (2011), doi:10.1109/ITSC.2011.6083138
Naumann, R., Rasche, R., Tacken, J., Tahedi, C.: Validation and simulation of a decentralized intersection collision avoidance algorithm. In: IEEE Conference on Intelligent Transportation System, ITSC (1997), doi:10.1109/ITSC.1997.660579
Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas. 41(2) (2008), doi:10.1007/s10817-008-9103-8
Platzer, A., Clarke, E.M.: Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 547–562. Springer, Heidelberg (2009)
Sheeran, M., Singh, S., Stålmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: Hunt Jr., W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
Sin, M.L., Bouroche, M., Cahill, V.: Scheduling of dynamic participants in real-time distributed systems. In: 30th IEEE Symposium on Reliable Distributed Systems, SRDS (2011), doi:10.1109/SRDS.2011.37
Slot, M., Cahill, V.: A reliable membership service for vehicular safety applications. In: IEEE Intelligent Vehicles Symposium, IV (2011), doi:10.1109/IVS.2011.5940487
Steiner, W., Dutertre, B.: SMT-Based Formal Verification of a TTEthernet Synchronization Function. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 148–163. Springer, Heidelberg (2010)
The World Bank. Road safety (2011), http://www.worldbank.org/transport/roads/safety.htm (accessed December 2011)
Tomlin, C., Pappas, G., Sastry, S.: Conflict resolution for air traffic management: a study in multiagent hybrid systems. IEEE Transactions on Automatic Control 43(4) (1998), doi:10.1109/9.664154
Traffic Accident Causation in Europe (TRACE) FP6-2004-IST-4. Deliverable 1.3 road users and accident causation (2009)
Verma, R., Vecchio, D.: Semiautonomous multivehicle safety. IEEE Robotics Automation Magazine 18(3) (2011), doi:10.1109/MRA.2011.942114
Zimmermann, A., Hommel, G.: A train control system case study in model-based real time system design. In: Proceedings. International Parallel and Distributed Processing Symposium, 2003 (2003), doi:10.1109/IPDPS.2003.1213234
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Asplund, M., Manzoor, A., Bouroche, M., Clarke, S., Cahill, V. (2012). A Formal Approach to Autonomous Vehicle Coordination. In: Giannakopoulou, D., Méry, D. (eds) FM 2012: Formal Methods. FM 2012. Lecture Notes in Computer Science, vol 7436. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32759-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-32759-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32758-2
Online ISBN: 978-3-642-32759-9
eBook Packages: Computer ScienceComputer Science (R0)