Getting the point — Obtaining and understanding fixpoints in model checking

Sjoerd Cranen

Promotors: prof.dr.ir. J.F. Groote (TU/e) and prof.dr. J.J. Lukkien (TU/e)
Copromotor: dr. S.P. Luttik (TU/e)
Technische Universiteit Eindhoven
Date: 17 June, 2015, 16:00

Summary

High-tech industry has become heavily reliant on correctly functioning software and logical circuits. A case in point is the automotive industry, where so-called by-wire techniques, implemented as hybrid hardware/software systems, replace and enhance mechanical solutions for steering and braking.

In this thesis, we investigate how model checking techniques based on fixpoint logic can help in analysing these systems, and how these techniques might be improved to make them easier to use.

Using existing technology, we analyse a part of the FlexRay communication protocol, which is used in the automotive industry to provide a communication channel between the various—sometimes safety-critical—parts of a car. A previously unknown error is uncovered by model checking the protocol under various fault models.

We then turn our attention the the process of model checking that was used in the FlexRay case study, and develop theory to address some of the pitfalls we encountered there. We leave the context of our case study, and address the following three issues.

• Using first order modal fixpoint logic, one can describe the desired behaviour of a system, as we demonstrated in the case study. While this logic is expressive enough to formulate the properties we are interested in, it can appear rather enigmatic to those with no background in fixpoint logic. We show that the more accessible logic CTL* can be translated succinctly into the logic that was used in the case study, and that model checking the translated formula has the same time complexity as solving the original formula with a CTL* model checker. The problem of translating CTL* to modal fixpoint logic is in itself interesting, because no succinct translation existed previously; known translations caused at least an exponential blowup in the size of the formula. The translation in this thesis is linear, because we use a first-order fixpoint logic.
• A major problem in model checking is that the size of the semantic model (a graph structure) of specifications of realistic industrial systems is often immense. Fixpoint logic formulas that encode model checking problems on such systems can be solved by generating a graph structure called a parity game, and calculating the solution to the model checking problem from this graph. These parity games also grow impractically large. We therefore investigate means to reduce the size of these games, while preserving their solution.
• Finally, we design a method to provide feedback to the user of a fixpoint model checker, by equipping fixpoint logic with a notion of evidence. In the FlexRay case study, it occurred that after two days of computing, the model checker returned with the answer `no’, where we expected it to be `yes’. With our notion of evidence, the model checker could also have indicated what part of the protocol we needed to look at to understand why the answer was `no’.

To make our results more generally applicable, the notion of evidence is defined for a fixpoint logic that generalizes LFP (least fixpoint logic), which extends first-order logic with a fixpoint operator, and PBES (parameterized Boolean equation systems), an equational fixpoint logic that underlies the model checker we used for our case study.