Model Checking

Last updated Apr 11, 2023 Edit Source

Inputs:

• description of the system
• property to verify The tool either confirms that the property is true in the model or informs the user that it does not hold. In that case, the model checker will also provide a counter-example: a run of the system that violates the property. This answer helps find the reason for the failure and has significantly contributed to the success of model checking in practice.

Transition systems describe the states, initial states and the possible state transition for the system.

Formally: $T=(Q,I,E,\delta)$

• $Q$ set of states
• $I$ set of initial states
• $E$ set of actions
• $\delta$ a transition relation $\delta \subset Q\times E\times Q$

A Kripke structure extends a transition system with the idea of propositions in states.

Formally: $K=(Q,I,E,\delta,\lambda)$

• $\lambda: Q\rightarrow2^V$, where $V$ is a set

Invariants are safety properties.

Formally: a system invariant is a property $P$ such that $q\models P$, for all reachable states $q$.

A simple Breadth First Search or Depth First Search algorithm to enumerate all possible states and check for an invariant violation. The search space is large. A few techniques can be employed:

• Reduction based: determine a subset of runs whose exploration guarantees the correctness invariant over the overall system
• Abstraction: construct a significantly smaller model whose correctness guarantees the correctness of the original model.

The properties/invariants we need to check are for example:

• Does (the reachable part of) K contain “bad” states, such as deadlock states where only the τ action is enabled, or states that do not satisfy an invariant?
• Are there executions of K such that, after some time, a “good” state is never reached or a certain action never executed (livelock)?

We can express these by combining Propositional Logic and temporal operators: Operators are defined on paths/traces of execution: They can also be nested: FG p: there exists a trace where eventually, p holds forever. Only the first trace can be proven to be true since we do not know the states of p for the 2nd trace.

Apply temporal logic not just on a single path but on many different possible branches which is needed for transition systems. Operators cannot be nested

A core tool used for model checking is NuSMV

• Symbolic Model Verifier (SMV)
• NuSMV: open source re-implementation

Data structure which efficiently reduces redundancy in sub-expressions of Boolean functions.

The basic state space search algorithm with set theory: This is useful in model checking as we can represent $R$ and $I$ as boolean function of {0,1} as being part of the set or not. We can then use BDD operations rather than set operations.

• Traverse BDD from bottom to top
• For each layer of variables, eliminate nodes with equal successors. Sort nodes and unite nodes with equal successors