Model Checking
objectives
The growing in complexity of software systems require even
more powerful and optimized tools for automatic
verification of desired properties. Traditional techniques
are usually not automated, too complex or give only
partial results: simulation and testing techniques are
devoted to analyze only selected portions of the system.
They can be a cost-efficient way to find many errors but
rarely they are used to find all the errors.
Model checking algorithms, instead, offer an
exhaustive and automatic approach to
completely analyze the system. In particular,
model checking techniques aim is to analyze
concurrent systems behavior with respect to selected
properties.
The system behavior is modeled through finite state
machines (in general, state-based machines) or through
higher level languages, like CCS, CSP, Lotos or SDL.
Properties may be expressed using Temporal Logic (Temporal
model checking) or in terms of Automata
(automata-theoretic model checking). The FSM model of the
system behavior is then exhaustively explored to check
that the system is a correct implementation of its
specification or it conforms to
the specification. If resources are enough, model checking
always terminate discovering and showing errors or proving
the system correctness. It always terminate since the
state-space is limited and finite (also if it can be
huge). Although the restriction to finite state systems
has some limitations, it allows to apply automatic
techniques for verification. Moreover, model checking is
applicable to several very important classes of systems.
Initially, model checking has been exclusively adopted to
verify the logical behavior of circuits described at the
Register Transfer Level. Nowadays, model checking
techniques are used to verify concurrent protocols,
process control systems, reactive systems [MC_Book].
The main advantages these techniques offer may be
summarized as follows:
- model checking is quite fast;
- model checking is exhaustive;
- tools may automatically perform model checking;
- if errors are found, counterexamples are provided.
Moreover, model checking is largely applied in practice to
such an extent that industry is introducing such
techniques in the system development process.
On the other side, model checking also suffers of some
limitations:
- it may only verify systems expressed through
state-based machines;
- it is more limited than theorem proving, but much
more easy to use;
- it suffers of the state explosion
problem: when the system is made up of a large number of
processes running in parallel, the model representing the
whole system may be composed of millions of states. The
model checking of the whole state space cannot be done if
the representation of the structure does not fit
into the available (memory and time) resources. Several
techniques have been studied to handle large state spaces,
reducing the data structure representation or abstracting
information: symbolic and on-the-fly
model checking, reduction and
compositional reasoning. They will be shortly
presented in the next section.
Model Checking Techniques
Techniques based on how properties are formalized:
Temporal Model Checking:
properties are expressed in terms of a propositional
temporal logic and logical formulae are capable to
describing the behavior of a system over time. Temporal
logics can describe ordering of event without introducing
time explicitily and are an effective tool to specify
reactive system properties [MC_Book]. There
are several flavors of temporal logics, each one with its
own model checking algorithm. CTL [Clarke83,Sifakis82] is
a branching-time logic, polynomial in the size and in the
length of its specification. In linear-time temporal logic
(LTL) time is
totally and linearly ordered, i.e., measured with natural
numbers.
The language of LTL is that of propositional calculus
augmented with four temporal operators: ``at the next
time", ``always", ``until" and ``eventually". The
complexity of these formulae is exponential in the length
of the formula but linear in the size of
the global state graph...
CTL* [Clarke83] is a very expressive logic that combines
both branching- and linear-time operators. More
information on CTL and CTL* may be found in [MC_Book].
Automata-theoretic methods [MC_Book]:
the property specification is modeled using an automaton.
The system (represented by an automaton) is compared to
the property specification (also represented by an
automaton) for conformance. Different kinds of conformance
have been explored: i) language inclusion [Kurshan94]: it
checks that the language of the system automaton is
contained in the language of the property automaton. ii)
equivalence checking [Cleaveland,Fernandez88]: the model
and the specification are checked with respect to some
equivalences, like observational, trace and branching.
iii) In refinement orderings [Cleaveland,Roscoe94]
specifications are
less detailed then the system. A system needs to supply at
least the behavior described by the specification and may
introduce details. iv) Successive refinement [Kurshan94]:
a succession of models of increasing details drive this
technique. The idea is that the more detailed model must
satisfy the properties the less detailed exposes.
Translating Temporal formulae into Automata
The approach proposed in [VardiWolper86] shows a point of
contact between automata-theoretic and temporal model
checking.
The authors show how the linear temporal logic model
checking problem could be formulated in terms
omega-automata.
Techniques to handle the state explosion problem:
On-the-fly verification:
an exhaustive search on the global system is usually
impossible for not trivial systems. On-the-fly techniques
are based on the observation that many states in the
system automaton may be generated only if needed; the
property automaton is constructed and it is used to drive
the construction of the system automaton.
Some system states may never be generated at all and the
process termination may arrives before completing the
system automaton construction. The system automaton is
generated using a depth-first visit. There is an important
trade-off between memory requirements and state space: i)
a depth first visit that stores
only the current path explored minimize the memory usage
but causes the regeneration of already visited states. ii)
A depth visit that stores all reached states, sensibly
reduces time but increases memory usage. State-space
caching [Holzmann87a] and supertrace
[Holzmann88,Holzmann95] techniques have been
presented to optimize memory and state space. In the
former technique, visited states are stored into a
cache. When it is full, different policies may be
adopted to replace old states with new ones. In the
latter, partial search of the state space is
performed.
An advantage of on-the-fly techniques is that if an error
is revealed, it stops and outputs the error trace. When no
errors are found, the search covers the entire state
space. Based on these considerations this techniques are
particularly suitable for early states of design,
containing several errors [Kerbrat94].
Reduction:
it is a technique to abstract the state space preserving
the ability to prove properties of interest. The main
approaches are: i) partial-order reduction
[GW91,Holzmann92,Peled94]: a partial-order technique
attempts to compute only those not redundant parts of the
state graph. It is based on the idea that
interleaving models of concurrent computations are very
wasteful,
since in many cases the specification is not influenced by
different ordering of the same commands. All possible
interleaving can be avoided, exploring a reduced graph
while preserving desired properties. In partial-order
methods, only a subset of all possible transitions enabled
from the current state ``s" are selected. The main
selection techniques are the persistent
sets and sleep sets. ii) Compositional
minimisation: given a system S, the compositional
minimization technique objective is to create the
minimized specification S' (and its graph) so
that S satisfies a property p iff S' satisfies p.
Obviously, the minimized graph modeling S' has to be
generated without first generating the complete graph of
the system. This technique enables the software analyst to
replace the complex system S with a more simple S' to
optimize the analysis and obtain the same results. iii)
Abstraction: when the initial model
is too complex to be reasonably analyzed then a more
abstract model may be built omitting some unrelevant
details and successively analyzed. Following this
definition, the compositional minimisation technique can
also be viewed as an
abstraction technique. The assumption the approach makes
is that
if the abstract model fulfills the specifications, also
the initial model satisfies the specifications. Naturally,
if the abstract model does not satisfy the specification,
it does not means that the initial model does not satisfy
it. It is to say that care must be done to create an
abstract model that preserves the specification. Several
abstraction techniques have been proposed in
[Kurshan94,BH97,CousotCousot99,Clarke96c].
Symbolic model checking:
In 1987 McMillan [Mc1,Mc2] understood that symbolic
representation of the system should be used to overcome
the state explosion problem in model checking. Symbolic
representation was based on Ordered Binary Decision
Diagrams (OBDDs) [OBDD}, data structures based on boolean
functions that can be used to
represent sets of state and sets of transitions between
states. An OBDD is similar to a binary decision tree but
its structure is a directed acyclic graph rather than a
graph. Symbolic model checking checks temporal formulae
directly to OBDD data structure, avoiding the construction
of the state graph of the concurrent
system explicitly. Using OBDDs is possible to verify
extremely large number of states thus allowing to analyze
systems composed of 10^120. In 1992, SMV [Mc2] (a model
checking system that extracts an OBDD for programs in the
SMV language) was used to construct a precise model of the
IEEE Futurebus+
[IEEEStand] standard: it was the first time an IEEE
standard has been automatically verified.
Compositional Reasoning:
it uses the concept of modularization to
handle the state explosion problem. The idea is to
decompose complex systems in different parts (e.g., simple
processes) and analyze each part separately, since each
part is smaller then the combination of all the parts
together. Global properties are decomposed in local
properties to be validated with respect to single modules.
Local properties are then combined to deduce global
properties. An obvious strategy is to check properties on
the system portion they involve. One way to create
modularity is to separate a process
from its environment; this method is known as
``assume-guarantee"
[Francez76,Jones83,Pneuli84]. This technique verifies each
component separately making assumptions on how the related
processes work (without the process itself). Simulation
relations are an important tool to mechanize modular
methods: if a formula is true in a model, then it is also
true in any model which is
smaller in the preorder. Compositional reasoning avoids
the construction of the complete-state space, offering one
of the most promising approach to limit state explosion;
on the other hand, it is usually complicated to decompose
global properties into local ones, proving that when local
properties are verified in
subsystems then global properties are true in the whole
system.
More details on model checking techniques may be found in
[DimitraTesi,MC_Book].
SPIN, Promela and LTL
Work leading to the SPIN [SPIN_W] verification tool
started in 1980 with Pan. It was a one-pass, on-the-fly,
verification system. In 1983 it was replaced by Trace: it
represents the change from a verification method based on
process algebras to one based on automata. This change was
done for efficiency considerations.
In 1987 Trace was replaced with Supertrace and in 1989 the
first version of SPIN was written. It has been extended in
subsequent years with reduction technique (Static
Reduction Method), LTL conversion and minimized automata
features.
SPIN is a state-based and on-the-fly
tool that uses partial order reduction
techniques to formal verifying and analyzing the logical
consistency of concurrent systems, specifically of data
communication protocols. Some of the SPIN
main features (described in [SPIN_W]) may be listed as
follow:
- SPIN targets efficient software verification: the
tool checks the logical
consistency of a specification reporting on deadlocks,
unspecified
receptions, flags incompleteness, race conditions, and
unwarranted
assumptions about the relative speeds of processes;
- SPIN can be used as a full LTL model checking
system, supporting all correctness requirements
expressible in linear time temporal logic;
- SPIN supports both rendezvous and buffered message
passing, and communication through shared memory;
- SPIN supports random, interactive and guided
simulation.
SPIN can be used in three basic modes:
- as a simulator which allows for rapid prototyping
with a random, guided, or interactive simulations;
- as an exhaustive state space analyzer, capable of
rigorously proving the validity of user specified
correctness requirements;
- as a bit-state space analyzer that can validate
even very large protocol systems with maximal coverage of
the state space.
The SPIN software is written in ANSI standard C. It is
portable across all versions of the UNIX operating system.
Xspin is a graphical front-end to drive SPIN.
SPIN uses a high-level language to specify systems
descriptions, called Promela (PROcess MEta LAnguage) [SPIN_W].
The system is described in a modeling language called
Promela. The language allows for the dynamic creation of
concurrent processes. Communication via message channels
can be defined to be synchronous (i.e., rendezvous), or
asynchronous (i.e., buffered).
The key elements used in the language are processes (proctypes),
message channels and variables: processes are global
objects while message channels and variables can be
declared either globally or locally within a process. Data
types, array variables, process types, process
instantiation and many other constructs may be defined in
Promela. Case selection, repetition, and unconditional
jumps are the main control flow constructs in Promela.
These and
many other Promela statements are described in [SPIN_W].
An example of Promela code follows:
1 mtype = {Wakeme, Running}; /* two symbolic names */
2
3 bit lk, sleep_q; /* boolean variables */
4 bit r_lock, r_want;
5 mtype State = Running; /* variable of type mtype */
6
7 active proctype client()
8 {
9 sleep: /* the sleep routine */
10 atomic { (lk == 0) -> lk = 1}; /* SPINlock(&lk) */
11 do /* while r.lock is set */
12 :: (r_lock == 1) -> /* r.lock == 1 */
13 r_want = 1; /* set the want flag */
14 State = Wakeme; /* remember State */
15 lk = 0; /* freelock(&lk) */
16 (State == Running); /* wait for wakeup */
17 :: else -> /* r.lock == 0 */
18 break /* break from do-loop */
19 od;
20 progress: /* progress label */
21 assert(r_lock == 0); /* should still be true */
22 r_lock = 1; /* consumed resource */
23 lk = 0; /* freelock(&lk) */
24 goto sleep
25 }
It has been borrowed by [Holz_TSE97] and represents a
client process that consumes resources that are provided,
one by one, by the server. The availability of a resource
is modeled here by a zero value of the global variable
r_lock. The client can set the value of r_lock to one
(line 22), but only the server can reset
it to zero (line 30). If the resource is unavailable (line
12), a flag is set to indicate the process’s needs (line
13), its state is changed (line 14), and it is put to
sleep by the operating system until it is re-awakened by
the server (line 16). The entire
sequence is performed after first setting (line 10) and
then releasing (lines 15 and 23) a spinlock that
guarantees exclusive access to this section of the code.
SPIN accepts correctness properties expressed in linear
temporal logic (LTL), i.e., SPIN may be used as a full LTL
model checking system, supporting all correctness
requirements expressible in linear time temporal logic. We
use correctness requirements to formalize system behaviors
that are claimed to be impossible,
i.e., to formalize the potential violation of correct
system behavior. Any LTL formula can be translated into a
Büchi automaton and SPIN automatically performs this
conversion using an on-the-fly construction. Correctness
properties can be specified as general linear temporal
logic requirements (LTL), either directly in the syntax of
LTL, or indirectly as Buchi Automata.
Each positive LTL formula can, of course, be turned into a
negative one, and vice versa, by prefixing it with a
logical negation operator. A positive claim requires us to
prove that the language of the system (i.e., all its
executions) is included in
the language of the claim. A negative claim, on the other
hand, requires us to prove that the intersection of the
language of the system and of the claim is empty.
The entire computation, starting from the individual
concurrent components and a single Buchi automaton
representing the correctness claim, is done by SPIN in one
single procedure, using a nested depth-first search
algorithm. The algorithm terminates when an acceptance
cycle is found (which then constitutes a
counterexample to a correctness requirement), or, when no
counter-example exists, when the complete intersection
product has been computed. More information on the
construction of LTL formulae may be found in [SPIN_W].
|
