Symmetry Based Model Checker
SMC is a symmetry based model checker that was developed at
University of Illinois at Chicago, Electric Engineering Department
under the coordination of
A. Prasad Sistla
with the contribution of
Viktor Gyuris.
The program employs the latest results on symmetry
for checking safety and liveness properties of concurrent
system of processes. The input to
the system consists of a concurrent program given as a set of processes
specified as transition
systems. It also takes as input a Buchi automaton on infinite strings that
accepts all the incorrect computations, that is, the automaton accepts the
complement of the correctness property.
The system checks if there exists a fair computation of the
program that is accepted by the automaton, i.e., if there
exists an incorrect computation. If such a computation exists
it outputs a ``YES'' answer, otherwise it terminates with a ``NO''
answer indicating that the program satisfies the correctness property.
SMC can handle both weak fairness and strong fairness.
The user can specify either option as part of the command line.
The program first reads the code of the concurrent program written in
the input language specified below as well as
the finite state automaton that provides the negation of the property to be
checked.
From the read code the compressed computation space, called
Annotated Quotient Structure (AQS), is constructed.
Finally, the product of the automaton and the AQS is constructed
(called the BBar structure) and a search for a reachable strongly
connected component is performed.
For brief introduction follow
SMC: A Symmetry based Model Checker for Verification of Safety and Liveness Properties.
For details on the theoretical
background, see
On-the-Fly Model checking under Fairness that
Exploits Symmetry.
Syntax of SMC
COMMAND: SMC [-s<num>][-o<num>][-v<num>][-f<C>][[-p] filename]
OPTIONS:
-s<num>
This parameter controls the symmetry
option. If the value of <num> is zero then symmetry compression
is not used. If the program has no symmetry then this option is the best.
If the value of <num> is 2 or 4 or 6 then only process symmetry
is employed. The higher the value, the more sophisticated is the equivalence
checking algorithm employed, resulting in fewer number of states in the
constructed structure.
If the value of <num> is 3 or 5 or 7 then both
process symmetry and state symmetry are employed. As before,
the higher the value, the more sophisticated is the employed
equivalence checking algorithm.
If the value of <num> is 3 then both process symmetry
and state symmetry are employed. This gives maximum compression but it also
has more overhead for detecting process as well as state symmetry.
-o<num> This parameter controls the on-the-fly
option. If the value of <num> is 0 then
on-the-fly option is used. If it is 1 then on-the-fly option is used.
-f<C> This parameter controls the fairness option.
Here <C> is a character with value "w" or "s". Value "w"
specifies weak fairness, while value "s" specifies strong fairness.
The default is weak fairness.
-v<num>This parameter allows counter example to be printed; it also allows printing of AQS, BBar states and transitions. It
controls the output verbosity.
Bit 0: basic information on performance.
Bit 1: the parsed input text is printed in a lengthy way.
Bit 2: information on each AQS state is printed.
Bit 3: counter example is printed. The counter example consists of
a strongly connected component in BBar and a path leading to it.
Bit 4: information on each BBar state is printed.
For example, an option value of 24 (where bits 3 and 4 have value 1)
prints all the BBar states and trasitions; it also prints a counter example.
[-p] filename Specifies the name of the program file.
Default is ClientServer.prg.
The C++ source code of the program can be downloaded
from here .
The Input language
The model checker assumes that the input program has the following
architecture:
processes are divided into modules;
all processes in a module are identical upto renaming,
that is, any permutation mapping processes
in a module to processes in the same module is a symmetry of the system.
Processes communicate through
shared variables. A shared variable between two processes is specified
by the name together with the indices of the processes.
If a process in a module C has a shared variable with another process
in module D, then every process in C has such a shared variable
with every process in D.
In expressions process indices are replaced by index variables.
The type of an index variable is a defined module, the range of the
index variable is 0,...,n-1 where n is the number
of instances of the type of that variable.
An input consists of commands separated by semicolon. A command is
one of module declaration, variable declaration, index variable declaration
or module description. All variables need to be declared, but index
variables can be declared implicitly. A module description is a set
of module commands. A module command is of the form condition ->
actions. A condition is an expression with positive value. An expression
is built from variables and constants using the following operands:
- arithmetical: + - * ? %,
- logical: < > <= >= == != <> and & or | not !,
- i == j and i != j where i and j
are index variables,
- <quantor>( <ind_var> : <expression>)
where <quantor> is one of ALL EXISTS AND OR PRODUCT
SUM NUMBEROF.
Finally, an action is either an assignment of a variable or a generalized
assignment.
The input language is defined by the following grammar:
program : Program commands
commands : commands command
| command
command : Module name = value ;
| name [ some_module_names ] = value ;
| ind_var : module
| ind_var ;
some_module_names :
| module_names
module_names : name
| name, module_names
ind_var : name
| name `of' name
module : { module_commands }
| module_command
module_commands : module_commands module_command
|
module_command : condition -> actions ;
actions : action
| action , actions
action : variable = condition
| ALL ( ind_var : actions )
An example program is the client server driver specification:
Program
Module controller = 1;
Module client = 49;
lc[controller] = 0;
lk[client] = 0;
reply[controller, client] = 0;
request[controller, client] = 0;
buzy[controller] = 0;
c of controller :
{
lc[c] == 0 & request[c, k] == 1 ->
reply[c, k] = 1, buzy[c] = 1 , lc[c] = 1;
lc[c] == 1 & buzy[c] == 0 ->
lc[c] = 0 ;
}
k of client :
{
lk[k] == 0 -> request[c, k] = 1 , lk[k] = 1;
lk[k] == 1 & reply[c, k] == 1 ->
reply[c, k] = 0, request[c, k] = 0, lk[k] = 2;
lk[k] == 2 -> buzy[c] = 0 , lk[k] = 0;
}
The language of the automata specification
The finite state automaton is given by enumerating its
transitions. A transition is of the form condition ->
auto_state : auto_state. In the first command the
initial state of the automaton need to be specified.
The final states can be specified any time. The list
of tracked processes is computed automatically, unless
it is manually specified. (For details on tracking consult
the mentioned paper).
automata : InitialState name ; a_commands
a_commands:
| a_command ; a_commands
a_command : FinalState
| FinalState a_fin_states
| Tracking
| Tracking a_trackings
| a_transition
a_fin_states : name
| name , a_fin_states
a_trackings : a_tracking
| a_tracking , a_trackings
a_tracking : number `of' name
a_transition : condition -> name : name
The Mutual Exclusion property for the
client server program is coded in the following example.
InitialState M0;
FinalState M1;
ALL(k1 of client: ALL(k2 of client: k1== k2 or lk[k1] + lk[k2] < 4)) -> M0:M0;
EXISTS(k1:EXISTS(k2: k1!=k2 & lk[k1]==2 & lk[k2]==2)) -> M0:M1;
True -> M1:M1;
Last updated April 11, 1997.