The input language of NuSMV is designed to allow the description
of finite state machines (FSM) which range from completely synchronous
to completely asynchronous, and from the detailed to the abstract.
One can readily specify a system as a synchronous Mealy machine, or as
an asynchronous network of nondeterministic processes. The language
provides for modular hierarchical descriptions, and for the definition
of reusable components. Since it is intended to describe finite state
machines, the only data types in the language are finite ones --
booleans, scalars and fixed arrays. Static, data types can also be
constructed.
Specifications can be expressed in CTL (Computation Tree Logic), or LTL (Linear Temporal Logic). These logics allow a rich class of temporal properties, including safety, liveness, fairness and deadlock freedom, to be specified in concise a syntax.
The primary purpose of the NuSMV input is to describe the
transition relation of a Kripke structure. Any expression in the
propositional calculus can be used to describe this relation. This
provides a great deal of flexibility, and at the same time a certain
danger of inconsistency. For example, the presence of a logical
contradiction can result in a deadlock -- a state or states with no
successor. This can make some specifications vacuously true, and makes
the description unimplementable. While the model checking process can
be used to check for deadlocks, it is best to avoid the problem when
possible by using a restricted description style. The NuSMV system
supports this by providing a parallel-assignment syntax. The semantics
of assignment in NuSMV is similar to that of single assignment data
flow language. By checking programs for multiple parallel assignments to
the same variable, circular assignments, and type errors, the
interpreter insures that a program using only the assignment mechanism
is implementable. Consequently, this fragment of the language can be
viewed as a description language, or a programming language.
Consider the following simple program in the NuSMV language.
MODULE main
VAR
request : boolean;
state : {ready, busy};
ASSIGN
init(state) := ready;
next(state) := case
state = ready & request = 1 : busy;
1 : {ready, busy};
esac;
SPEC
AG(request -> AF state = busy)
The first part defines the Kripke structure. The space of states of the
Kripke structure is determined by the declarations of the state
variables (in the above example request and state). The
variable request is declared to be of (predefined) type
boolean. This means that it can assume the (integer) values
0 and 1. The variable state is a scalar variable,
which can take the symbolic values ready or busy.
The following assignment sets the initial value of the variable
state to ready. The initial value of request is
completely unspecified, i.e. it can be either 0 or 1.
The transition relation of the Kripke structure is expressed by defining
the value of variables in the next state (i.e. after each transition),
given the value of variables in the current states (i.e. before the
transition). The case segment sets the next value of the variable
state to the value busy (after the column) if its current
value is ready and request is 1 (i.e. true).
Otherwise (the 1 before the column) the next value for
state can be any in the set {ready,busy}.
The variable request is not assigned. This means that there are
no constraints on its values, and thus it can assume any value.
request is thus an unconstrained input to the system.
The keyword `SPEC' is followed by a CTL formula, that is intended to
be checked for truth in the Kripke structure defined above. The
intuitive reading of the formula is that every time request
is true, then in all possible future evolution, eventually state
must become busy.
The following program illustrates the definition of reusable modules and expressions. It is a model of a three bit binary counter circuit. The order of module definitions in the input file is not relevant.
MODULE counter_cell(carry_in) VAR value : boolean; ASSIGN init(value) := 0; next(value) := value + carry_in mod 2; DEFINE carry_out := value & carry_in; MODULE main VAR bit0 : counter_cell(1); bit1 : counter_cell(bit0.carry_out); bit2 : counter_cell(bit1.carry_out); SPEC AG AF bit2.carry_out
The Kripke structure is defined by instantiating three times the module
type counter_cell in the module main, with the names
bit0, bit1 and bit2 respectively. The
counter_cell module has one formal parameter carry_in. In
the instance bit0, this parameter is given the actual value
1. In the instance bit1, carry_in is given the
value of the expression bit0.carry_out. This expression is
evaluated in the context of the main module. However, an
expression of the form `a.b' denotes component
`b' of module `a', just as if the module
`a' were a data structure in a standard programming
language. Hence, the carry_in of module bit1 is the
carry_out of module bit0.
The keyword `DEFINE' is used to assign the expression value &
carry_in to the symbol carry_out. A definition can be thought of
as a variable with value (functionally) depending on the current values
of other variables. The same effect could have been obtained as follows
(notice that the current value of the variable is assigned,
rather than the next value.):
VAR carry_out : boolean; ASSIGN carry_out := value & carry_in;
Defined symbols do not require introducing a new variable into the BDD representation of the system. However, they cannot be given values non-deterministically. Another difference between defined symbols and variables is that while the type of variables is declared a priori, for definitions this is not the case.
The previous examples describe synchronous systems, where the
assignments statements are taken into account parallel and
simultaneously. NuSMV allows to model asynchronous systems. It
is possible to define a collection of parallel processes, whose actions
are interleaved, following an asynchronous model of concurrency. This
is useful for describing communication protocols, or asynchronous
circuits, or other systems whose actions are not synchronized (including
synchronous circuits with more than one clock region).
The following program represents a ring of three asynchronous inverting gates.
MODULE inverter(input) VAR output : boolean; ASSIGN init(output) := 0; next(output) := !input; MODULE main VAR gate1 : process inverter(gate3.output); gate2 : process inverter(gate1.output); gate3 : process inverter(gate2.output); SPEC (AG AF gate1.out) & (AG AF !gate1.out)
Among all the modules instantiated with the process keyword, one
is nondeterministically chosen, and the assignment statements declared
in that process are executed in parallel. It is implicit that if a given
variable is not assigned by the process, then its value remains
unchanged. Because the choice of the next process to execute is
non-deterministic, this program models the ring of inverters
independently of the speed of the gates. For each gate, the
specification of this program states that the output of the gate
oscillates (i.e. that its value is infinitely often 0, and
infinitely often 1). In fact, this specification is false, since
the system is not forced to eventually choose a given process to
execute, hence the output of a given gate may remain constant,
regardless of its input.
In order to force a given process to execute infinitely often, we can
use a fairness constraint.
A fairness constraint restricts the attention of the model checker to
only those execution paths along which a given CTL formula is true
infinitely often. Each process has a special variable called
running which is 1 if and only if that process is
currently executing.
By adding the declaration:
FAIRNESS running
to the module inverter, we can effectively force every
instance of inverter to execute infinitely often, thus making the
specification true.
The alternative to using processes to model an asynchronous circuit would be to have all gates execute simultaneously, but allow each gate the non-deterministic choice of evaluating its output, or keeping the same output value. Such a model of the inverter ring would look like the following:
MODULE main VAR gate1 : inverter(gate3.output); gate2 : inverter(gate2.output); gate3 : inverter(gate1.output); SPEC (AG AF gate1.out) & (AG AF !gate1.out) MODULE inverter(input) VAR output : boolean; ASSIGN init(output) := 0; next(output) := !input union output;
The union operator (set union) coerces its arguments to
singleton sets as necessary. Thus, the next output of each gate
can be either its current output, or the negation of its
current input -- each gate can choose non-deterministically
whether to delay or not. As a result, the number of possible
transitions from a given state can be as
@ifnottex
2^n
, where n is the number of gates. This sometimes (but not always)
makes it more expensive to represent the transition relation.
The following program is another example of asynchronous
model. It uses a variable semaphore to implement mutual exclusion
between two asynchronous processes. Each process has four states:
idle, entering, critical and exiting. The
entering state indicates that the process wants to enter its
critical region. If the variable semaphore is 0, it goes
to the critical state, and sets semaphore to 1. On
exiting its critical region, the process sets semaphore to
0 again.
MODULE main
VAR
semaphore : boolean;
proc1 : process user(semaphore);
proc2 : process user(semaphore);
ASSIGN
init(semaphore) := 0;
SPEC
AG !(proc1.state = critical & proc2.state = critical)
MODULE user(semaphore)
VAR
state : {idle, entering, critical, exiting};
ASSIGN
init(state) := idle;
next(state) :=
case
state = idle : {idle, entering};
state = entering & !semaphore : critical;
state = critical : {critical, exiting};
state = exiting : idle;
1 : state;
esac;
next(semaphore) :=
case
state = entering : 1;
state = exiting : 0;
1 : semaphore;
esac;
FAIRNESS
running
If any of the specification is false, the NuSMV model
checker attempts to produce a counterexample, proving that the
specification is false. This is not always possible, since formulas
preceded by existential path quantifiers cannot be proved false by a
showing of a single execution path.
Similarly, sub-formulas preceded by universal path quantifier
cannot be proved true by a showing of a single execution path. In
addition, some formulas require infinite execution paths as
counterexamples. In this case, the model checker outputs a looping
path up to and including the first repetition of a state.
In the case of the semaphore program, suppose that the specification were changed to:
AG (proc1.state = entering -> AF proc1.state = critical)
In other words, we specify that if proc1 wants to enter its
critical region, it eventually does. The output of the model checker
in this case is shown in the figure below (1).
-- specification -- AG (proc1.state = entering -> AF proc1.state = critical) -- is false -- as demonstrated by the following execution sequence state 1.1: semaphore = 0 proc1.state = idle proc2.state = idle state 1.2: [executing process proc1] -- loop starts here -- state 1.3: proc1.state = entering state 1.4: [executing process proc2] state 1.5: [executing process proc2] proc2.state = entering state 1.6: [executing process proc1] semaphore = 1 proc2.state = critical state 1.7: [executing process proc2] state 1.8: [executing process proc2] proc2.state = exiting state 1.9: semaphore = 0 proc2.state = idle
The counterexample above shows a path with proc1 going
to the entering state, followed by a loop in which proc2
repeatedly enters its critical region and then returns to its
idle state, with proc1 only executing while proc2
is in its critical region. This path shows that the specification is
false, since proc1 never enters its critical region. Note that in
the printout of an execution sequence, only the values of variables that
change are printed, to make it easier to follow the action in systems
with a large number of variables.
NuSMV allows to specify the Kripke structure directly in terms of
propositional formulas. The set of possible initial states is specified
as a formula in the current state variables. A state is initial if it
satisfies the formula. The transition relation is directly specified as
a propositional formula in terms of the current and next
values of the state variables. Any current state/next state pair is in
the transition relation if and only if it satisfies the formula.
These two functions are accomplished by the `INIT' and `TRANS'
keywords. As an example, here is a description of the three inverter
ring using only TRANS and INIT:
MODULE main VAR gate1 : inverter(gate3.output); gate2 : inverter(gate1.output); gate3 : inverter(gate2.output); SPEC (AG AF gate1.output) & (AG AF !gate1.output) MODULE inverter(input) VAR output : boolean; INIT output = 0 TRANS next(output) = !input | next(output) = output
According to the TRANS declaration, for each inverter,
the next value of the output is equal either to the negation of
the input, or to the current value of the output. Thus, in
effect, each gate can choose non-deterministically whether or not to
delay.
Using TRANS and INIT it is possible to specify
inadmissible Kripke structures, where the set of initial states is empty
or the transition relation is not total. This may result in logical
absurdities.
Go to the first, previous, next, last section, table of contents.