3 Verification by Model Checking¶

3.1 Motivation for verification¶

Formal verification techniques consist of three part:

A framework for modelling systems, typically a description language of some sort; \(\mathcal{M}\)
A specification language for describing the properties to be verified; \(\phi\)
A verification method to establish whether the description of a system satisfies the specification. \(\mathcal{M}, s \vDash \phi\) holds?

Approaches to verification can be classfied according to the following criteria:

Proof-based vs. model-based;
Degree of automation;
Full- vs. property-verification;
Pre- vs. post-development.

Model checking:

Automatic, model-based, property-verification approach;
Be used for concurrent, reactive systems;
Concurrency bugs are among the most difficult to find by testing, since they tend to be non-reproducible or not covered by test cases;
Based on temporal logic
- A formula is not statically true or false in a model, as it is in propositional logic and predicate logic.
- The models of temporal logic contain several states and a formula can be true in some states and false in others.
- The static notion of truth is replaced by a dynamic one.
- The models \(\mathcal{M}\) are transition systems and the properties \(\phi\) are formulas in temporal logic.
- Model checker with the inputs \(\mathcal{M}\) and \(\phi\)

Temporal logic:

Linear-time logics (LTL) think of time as a set of paths, where a path is a sequence of time instances.
Branching-time logics (CTL) appears to make the non-deterministic nature of the future more explicit.
Another quality of time is whether we think of it as being continuous or discrete.

3.2 Linear-time temporal logic¶

3.2.1 Syntax of LTL¶

"definition"

It models time as a sequence of states (path), extending infinite to the future.

temporal connectives: X, F, G, U, R and W

X: neXt state
F: some Future state
G: all future states (Globally)
U: Until
R: Release
W: Weak-until

3.2.2 Semantics of LTL¶

"Semantics"

Use mathematical symbols (functions and relations) to represent the meaning of the formulas.

"Definition: Transition System"

\(\mathcal{L}\) is a labelling fucntion, and it is just an assignment of truth values to all the propositional atoms, as it was the case for propositional logic (valuation). We can replace values with labels.

\(\mathcal{P}(Atoms)\) is the power set of Atoms.

Example

example program
bit a[2];
a = 0;
while (1)
    a++;

transition system

graph LR;

A[00] --> B[01];
B --> C[10];
C --> D[11];
D --> A

\(\mathcal{M} = (S, \to)\)

\(S = {00, 01, 10, 11}\)

\(\to = {(00, 01), (01, 10), (10, 11), (11, 00)}\)

Example

\(S = \{S_0, S_1, S_2\}\)

\(\to = \{ (S_0, S_1), (S_0, S_2), (S_1, S_0), (S_1, S_2), (S_2, S_2) \}\)

\(L(S_0) = \{ p, q \}, L(S_1) = \{ q, r \}, L(S_2) = \{ r \}\)

The semantic of the model. (An infinite tree of all computation paths):

"What does \(\mathcal{M} \vDash \phi\) mean?"

\(\phi\) is a temporal logic formula specification. Whenever a request is made, it will be satisfied in the future. Linear-time temporal logic (LTL)

\(\mathcal{M}\) is a model/system/program. In model checking, we use labelled transition system (LTS) to represent \(\mathcal{M}\).

\(\vDash\) is a set of algorithms.

"Why we need Type System?"

Fully correctness is note pratical, so a light-weight correctness is needed. Type System is a light-weight method to check correctness.

Fully Correctness	Type System
Check every value of the model.	Property-oriented verification. Type is a property.

Size does matter for practical.

"Definition: Path"

Considering the path \(\pi = S_1 \to S_2 \to \dots\), we write \(\pi^i\) for the suffix starting at \(s_i\). e.g., \(\pi_3\) is \(s_3 \to s_4 \to \dots\)

Path means a possible running instance (behavior) of a program.

From another perspective, a program is a set of path. So we can use the Compactness Theorem to verify the infinite paths.

Automata: We can use finite symbols to define the infinite behaviors. (compact representation) => We can use transition system to represent infinite paths.

"Definition: Semantics of LTL"

If \(\mathcal{M}\) is clear from the context, we may abbreviate \(\mathcal{M}, s \vDash \phi\) by \(s \vDash \phi\)

Synchronized System vs. real-time system

In synchronized system, we don't care about how many time does it take to get from s0 to s1

3.2.3 Practical patterns of specifications¶

Safety: Something bad will not happen

Example:

\(G \neg (x_1 = x_2)\)
\(G \neg((x = 0) \land (y = z / x))\)

Patterns:

\(G \neg \phi\)

Liveness: Something good will happen

Examples:

\(F(cash > 100, 000, 000)\)
\(G(start -> F \; terminate)\)

Patterns:

\(F \; \phi\)
\(G \; F \; \phi\)

Strong fairness

If something is attempted/requested infinitely often, it will be successful/allocated infinitely often.

Example: \(G \; F \; ready -> G \; F \; run\)

3.2.4 Important equivalences between LTL formulas¶

3.3 Model checking: sysmtem, tools, properties¶

The model is an abstract representation of program.

3.3.1 Example: mutual exclusion¶

"Mutual Exclusion"

When concurrent processes share a resource, it may be necessary to ensure that they do not have access to it at the same time.

Problem: Find a protocol for determining which process is allowed to enter its critical section at which time.

Verification: Vefify our solution by checking that it has some expected properties, such as safety, liveness, non-blocking and no strict sequencing.

Model:

Model two processes, each of which is in its:
- non-critical state (n),
- or trying to enter its critical state (t),
- or in its critical state ©.
Each individual process undergoes transition in the cycle \(n \to t \to c \to n \to \dots\)
However, the two process interleave with each other

graph LR;
A[n] --> B[t];
B --> C[c];
C --> A;

Properties:

Safety: \(G \; \neg(c_1 \land c_2)\)
Liveness: \(G \; (t_1 \to F \; c_1)\)
Non-blocking: Not expressible in LTL. For every state satisfying \(n_1\), there is a successor satisfying \(t_1\).
No strict sequencing:
- There is a path with two distinct states satisfying \(c_1\) such that no state in between them has that property.
- Complement: All paths having a \(c_1\) period which ends cannot have a further \(c_1\) state until a \(c_2\) state occurs.
- \(\neg \; G(c_1 \to c_1 \; W \; (\neg c_1 \land \neg c_1 \; W \; c_2))\)
  - e.g., strict sequencing: \(n_1, t_1, c_1, c_1, n_1, n_2, t_2, c_2\)
  - e.g., no strict sequencing: \(n_1, t_1, c_1, c_1, n_1, t_1, c_1, c_1\)

3.3.2 The NuSMV model checker¶

Ref: https://nusmv.fbk.eu

NuSMV - New Symbolic Model Verifier

NuSMV provides a language for describing the models we have been drawing as diagrams and it directly checks the validity of LTL and CTL formulas on those models.

NuSMV takes as input a text consisting of a program describing a model and some specifications (temporal logic formulas). It produces as output either the word 'true' if the specifications holds, or a trace showing why the specification is false for the model represented by our program.

Modules in SMV

NuSMV supports breaking a system description into several modules, to aid readability and to verify interaction properties.
In model checking, paths are infinite by definition. However, the number of states is finite. Hence we have to use loops to check the model.

Synchronous and asynchronous composition

Modules in SMV are composed synchronously by default.
This means that there is a global clock and, each time it ticks, each time it ticks, each of the modules asynchronously.
By use of the process keyword, it is possible to compose the modules asynchronously.
In that case, processes run at different 'speed', interleaving arbitrarily.
At each tick of the clock, one of them is non-deterministically chosen an executed for one cycle.