Fixpoint Model Checking Safety Properties of Linear Hybrid Systems with Large Discrete State Spaces

13. März 2017, 16:15 , 17:45

Veranstalter:  Boris Wirtz, Universität Oldenburg
Ort:  OFFIS, Escherweg 2, Raum F02

Abstract:
Cyberphysical systems play an increasingly important role in every day life. If used in a safety critical context,
a system failure or incorrect behaviour may cause serious harm and even endanger human lifes.
Therefore safety critical cyberphysical systems, which typically consist of a continuous plant and (often)
complex discrete controllers, need to be designed and developed with great care, so that unnecessary errors
and design flaws are avoided.
Thus the use of formal methods in the development process is of utter importance. While model based development
is used also in the industrial development of hybrid systems, verification is rarely done.
One of the obstacles lies in the absence of an easy to use formalism. Hybrid Automata are the defacto
standard formalism, but since they lack explicit discrete data, and only allow a single discrete step between
flows, embedding of complex discrete controllers is not intuitive.
We present an improved system model, along with an algorithm for model checking safety properties symbolically.
Finally we introduce two optimization techniques :
Acceleration at once (AAO) aims at the parallel composition problem in hybrid system model checking :
Usually fixpoint model checking algorithms perform flow image computation iteratively - for each mode of
the model a mode image is computed separately, then all mode images are assembled to a global image. For
a model with multiple components this has the consequence, that global modes need to be generated by
computing the cross product of the component modes, leading to an exponential growth in the number of
global modes AND model checking cost.
AAO performs global flow image computation in a single sweep, thus avoiding iteration and cross product
computation, and reducing model checking costs considerably.
The epsilon-bloating optimization aims at reducing the costs of single model checking steps. The single
step costs mainly depend on the complexity of the state set representations. We try to replace state sets
with complex representations by overapproximations with simpler representations, thus lowering the model
checking costs. This comes with a prize – the overapproximation may cause spurious counterexamples,
which need to be identified and eliminated. Therefore the optimized model checking procedure is embedded
within a counterexample guided abstraction refinement (CEGAR) loop.
Betreuer: Prof. Dr. Werner Damm