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 Prasad. A. Sistla with the contribution of Leonidas Miliades and Viktor Gyuris.

The program demonstrates the latest results on how the symmetry of a concurrent program can be utilized in compressing the computation space. 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.

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 Liveness Properties. For details on the theoretical background, see On-the-Fly Model checking under Fairness that Exploits Symmetry.

Syntax of SMC

SYNOPSIS: SMC [-s<num>][-v<num>][[-p] filename]

OPTIONS:
-s<num>

-s<num> [-p] filename 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 specificed 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:

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.