SMI

1 2 3

With SMI, a system is described as a network of communicating processes, each process being an extended finite state automaton. Given the system textual description, the SMI routines build an equivalent symbolic representation using decision diagrams. This representation can be the starting point in the development of more customized applications, e.g. model checking for different temporal logics or symbolic minimization with respect to equivalence relations.

 Principles

The input language

The primary purpose of the SMI input language is to allow a natural and concise description of processes and their communications. Secondly, this description must be simple enough to be used for the construction of a symbolic representation using decision diagrams(DD). Some of the input language concepts are sketched in the following.

A process encapsulates data and behavior. It is specified by its variables, its communication ports and one or more control threads.

Variables are used to store local information about the process. Currently, only variables with simple finite domains are allowed: booleans, bounded naturals and other finite sets. The scope of a variable is the process definition,i.e. variables cannot be shared between different processes.

A thread is defined as a finite state automaton whose transitions can test and assign process variables. Furthermore, a transition can contain a message emission/receptionto/from one communication port. If a process contains more than one thread, they are completely asynchronous. The process executes a step by non-deterministically choosing a thread, then executing one of its enabled transitions. Note however that different threads can share the same process variables.

A protocol is specified by a composition expression whose ground terms are processes. Two operators are provided, one for parallel composition with synchronization by message emissions and receptions, and the other for abstractionof communication at some ports. The synchronization forces two or more transitions from different processes to be combined and executed simultaneously (rendez-vous). The abstraction hides or ignores the communication at some ports.

The symbolic model

The protocol model is a labeled transition system (Q, Act, (T_a | a in Act), Qo). Q is a finite set of states, Act is a set of actions, T_a subset of Q x Q is the transition relation labeled by a and Qo subset of Q is the set of initial states. Usually, such model underlies the protocol verification algorithms. Given a protocol described in our input language, our aim is to build and to handle efficiently its corresponding model.

The symbolic model interface was designed to allow the manipulation of model state sets and transitions, symbolically represented by decision diagrams (DDs).

The symbolic model is builded from a protocol described using the input language. More precisely, the protocol transition relations Ta are encoded using DDs. The encoding process can take into account a number of parameters. For example, the parallel composition and abstraction semantics can be considered CSP-like (with binary rendez-vous and CSP restriction) or CCS-like (with n-ary rendez-vous and CCS abstraction). We can also impose the computation of reachable states Acc - some verification algorithms are more efficient when the reachable states are a priori known.

Basic operations on sets, such as union, intersection or complementation are directly mapped to DDs functions. The inclusion or the equality test are straightforward using DDs. Some specialized functions which perform model exploration, e.g. to compute the initial state set Qo, or the successors/predecessors for a given state set, Post and Pre are also provided.

Finally, SMI is not based on one particular DD implementation, thus it can be used with any DDs and only a minimal interface is required.

 Applications

Mu-Calculus Model-Checker

The model checker performs the backward evaluation of alternating free mu-calculus formulae over symbolic model representations.

Intuitively, the semantics of a formula P represents the set of states which satisfy it and is noted by P. The model checking algorithm for a formula Po works in two steps:

• the set Po is constructed recursively over the formula structure.
• a decision procedure is invoked :
  — standard evaluation -:- checks if Qo is subset of Po
  — forward analysis -:- checks if Acc intersected with Po is not empty
  — invariant checking -:- checks if Qo is subset of Po and Post(Po) is subset of Po

Minimal Model Generator

Given a labeled transition system(LTS) the minimal model generator(MMG) generates an equivalent minimal LTS. The minimality is relative to a bisimulation equivalence. A precise and complete description of the MMG algorithm can be found in Bouajjani-Fernandez-Halbwachs-90.

Briefly, the principle of the MMG algorithm is to refine an initial partition of the state space until a reachable and stable partition is obtained. It can be also defined as a computation of the greatest fixed point of a splitfunction defined over partitions. Different reductions (by strong, weak, branching,... bisimulation) are obtained considering an appropriate splitfunction.

The algorithm can work with the symbolic model representations. More precisely, a symbolic representation of partitions can be used, i.e. representing each equivalence class by a decision diagram. All partition transformations are then reduced to classical operations on decision diagrams. Currentlly, an operational version of this algorithm works with the SMI library.

1 2 3