Home > Research > Publications & Outputs > Modular Verification of Vehicle Platooning with...

Links

Text available via DOI:

View graph of relations

Modular Verification of Vehicle Platooning with Respect to Decisions, Space and Time: Formal Techniques for Safety-Critical Systems. FTSCS 2018

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNChapter (peer-reviewed)peer-review

Published
Close
Publication date2/02/2019
Host publicationFormal Techniques for Safety-Critical Systems: 6th International Workshop, FTSCS 2018, Gold Coast, Australia, November 16, 2018, Revised Selected Papers
EditorsCyrille Artho, Peter Csaba Ölveczky
Place of PublicationCham
PublisherSpringer
Pages18-36
Number of pages19
ISBN (electronic)9783030129880
ISBN (print)9783030129873
<mark>Original language</mark>English

Publication series

NameCommunications in Computer and Information Science
PublisherSpringer
Volume1008

Abstract

The spread of autonomous systems into safety-critical areas has increased the demand for their formal verification, not only due to stronger certification requirements but also to public uncertainty over these new technologies. However, the complex nature of such systems, for example, the intricate combination of discrete and continuous aspects, ensures that whole system verification is often infeasible. This motivates the need for novel analysis approaches that modularise the problem, allowing us to restrict our analysis to one particular aspect of the system while abstracting away from others. For instance, while verifying the real-time properties of an autonomous system we might hide the details of the internal decision-making components. In this paper we describe verification of a range of properties across distinct dimensions on a practical hybrid agent architecture. This allows us to verify the autonomous decision-making, real-time aspects, and spatial aspects of an autonomous vehicle platooning system. This modular approach also illustrates how both algorithmic and deductive verification techniques can be applied for the analysis of different system subcomponents.