Formal probabilistic analysis of cyber-physical transportation systems

Authors Atif Mashkoor
O. Hasan
Editors B. Murgante et al.
Title Formal probabilistic analysis of cyber-physical transportation systems
Booktitle Cumputational Science and Its Applications - Proc. ICCSA 2012, Part III
Type in proceedings
Publisher Springer
Series Lecture Notes in Computer Science
Volume 7335
Department PQE
ISBN 978-3-642-31136-9
Month June
Year 2012
Pages 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.