Zone State Diagrams
Michael Gerke
This thesis presents a model of FlexRay’s physical layer protocol and a suitable data structure for model checking such models.
The FlexRay standard, developed by a cooperation of leading companies in the automotive industry, is a robust communication protocol for distributed components in modern vehicles. The key challenge in the analysis is that the correctness of FlexRay’s physical layer protocol relies on the interplay of the bit-clock alignment mechanism with the precise timing behavior of the underlying asynchronous hardware. This thesis presents a timed automata model of the physical layer protocol and the underlying hardware.
Model checking such data-intensive systems using a semi-symbolic state space representation, which represents timing information symbolically but discrete information explicitly, turns out to be infeasible. To overcome this problem, this thesis presents Zone State Diagrams (ZSDs), a novel data structure combining difference bound matrices with reduced ordered binary decision diagrams. In terms of the size of the instances that can be handled, the performance of a model checker using ZSDs is better than the standard semi-symbolic approach on several benchmarks and the FlexRay model, and sometimes even better than UPPAAL, e.g., in the case of the FlexRay model. While UPPAAL is the fastest on all benchmarks, ZSDs are often a bit slower than the standard semi-symbolic approach.
ZSDs represent the discrete part of the state space symbolically as well as the timed part. Thus data-intensive state spaces can be more efficiently represented with ZSDs than with semi-symbolic state space representations, as used, e.g., by UPPAAL.
Master Thesis.