Thumbnail Image
Publication

A formal approach to autonomous vehicle coordination

Date
2012
Abstract
Increasing demands on safety and energy e ciency will re- quire higher levels of automation in transportation systems. This in- volves dealing with safety-critical distributed coordination. In this paper we demonstrate how a Satis ability 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 ap- proach 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 auto- matically veri ed using the Z3 theorem prover.
Supervisor
Description
peer-reviewed
Publisher
Springer
Citation
18th International Symposium on Formal Methods;
Collections
Lero - The Science Foundation Ireland Research Centre for Software
Show all metadata
Files
Thumbnail Image
2012_Asplund.pdf
Adobe PDF, 375.02 KB
Keywords
automation transportation systems, Satisfiability Modulo Theories, vehicular coordination problem
ULRR Identifiers
https://hdl.handle.net/10344/2540
 https://doi.org/10.34961/853
Funding code
Funding Information
Science Foundation Ireland (SFI)
Sustainable Development Goals
External Link
License
Embedded videos