A formal approach to autonomous vehicle coordination

dc.contributor.author	Asplund, Mikael
dc.contributor.author	Manzoor, Atif
dc.contributor.author	Bouroche, Mélanie
dc.contributor.author	Clarke, Siobhán
dc.contributor.author	Cahill, Vinny
dc.date.accessioned	2012-09-17T13:18:00Z
dc.date.available	2012-09-17T13:18:00Z
dc.date.issued	2012
dc.identifier.uri	http://hdl.handle.net/10344/2540
dc.description	peer-reviewed	en_US
dc.description.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.	en_US
dc.language.iso	eng	en_US
dc.publisher	Springer	en_US
dc.relation.ispartofseries	18th International Symposium on Formal Methods;
dc.relation.uri	http://dx.doi.org/10.1007/978-3-642-32759-9_8
dc.rights	The original publication is available at www.springerlink.com	en_US
dc.subject	automation transportation systems	en_US
dc.subject	Satisfiability Modulo Theories	en_US
dc.subject	vehicular coordination problem	en_US
dc.title	A formal approach to autonomous vehicle coordination	en_US
dc.type	info:eu-repo/semantics/conferenceObject	en_US
dc.type.supercollection	all_ul_research	en_US
dc.type.supercollection	ul_published_reviewed	en_US
dc.contributor.sponsor	SFI	en_US
dc.relation.projectid	10/CE/I1855
dc.rights.accessrights	info:eu-repo/semantics/openAccess	en_US