Formal probabilistic analysis of cyber-physical transportation systems

Autoren Atif Mashkoor
O. Hasan
Editoren B. Murgante et al.
Titel Formal probabilistic analysis of cyber-physical transportation systems
Buchtitel Cumputational Science and Its Applications - Proc. ICCSA 2012, Part III
Typ in Konferenzband
Verlag Springer
Serie Lecture Notes in Computer Science
Band 7335
Abteilung PQE
ISBN 978-3-642-31136-9
Monat June
Jahr 2012
Seiten 419-434
SCCH ID# 1212

Formal specification and verification of cyber-physical transportation systems is inherently a complex task. A fail-safe specification of such systems not only includes intricate formalizations of assumptions and requirements but also a fine-grained analysis of their unpredictable and random components, at times at different levels of abstraction. Traditional techniques of verification and validation, such as simulation or model checking, do not cope very well with the posed challenges. In fact, sometimes it becomes merely impossible to guarantee certain properties, such as liveness, under all possible scenarios. We propose an approach based on higher-order logic for formal modelling and reasoning of cyberphysical transportation systems. In this approach, we express the unpredictable elements of the model by appropriate random variables. Instead of guaranteeing absolute correctness, these randomized models can then be used to formally reason about the probability or expectation of the system meeting its required specification. For illustration purposes, the paper presents a simple analysis of a vehicle platoon control algorithm.