| 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. |