The Sigali Tool Box

Overview of the tool

Sigali is a model-checking tool-based which manipulates ILTS: Implicit Labeled Transition Systems (which can be seen as an equational representation of an automaton) as intermediate models for discrete event systems. It offers functionalities for verification of reactive systems and discrete controller synthesis. It is developed jointly by Espresso and Vertecs.

The techniques used consist in manipulating the system of equations instead of the sets of solution, which avoids the enumeration of the state space. Each set of states is uniquely characterized by a polynomial and the operations on sets can be equivalently performed on the associated polynomials. Therefore, a wide spectre of properties, such as liveness, invariance, reachability and attractivity can be checked. Many algorithms for computing predicates states are also available.

Contact: Hervé Marchand.

The Controller Synthesis methodology

Control theory of discrete event systems allows to use constructive methods, that ensure, a priori, required properties on the system behavior. In this approach, the validation phase is reduced to properties not guaranteed by the programming process. Starting from a representation of the possible behaviors of the system(e.g. in the form of a finite state automaton) and the properties that have to be satisfied by the controlled system, the synthesis produces directly the constrained automaton, i.e., the one that presents only those behaviors that satisfy the required properties.

In our framework, The system is represented by an ILTS while the control of the system is performed by restricting the controllable input values to values suitable for the control goal. This restriction is obtained by incorporating new algebraic equations into the initial system.

Using symbolic methods (based on BDD techniques, avoiding state space enumeration), The various control objectives for which we are able to synthesize a controller are the following:


Sigali Tool Box

Sigali is a tool box that manipulates (sets of) variables and predicates by means of (predefined) functions using a Mathematica-based language. Using Sigali, one can create predicates over a set of variables. There exists functions to manipulate them (intersection, union, complementary, test of inclusion, etc). Some functions are used to replace some variables in a predicate by other predicates. All these operations are extended to the manipulation of lists of predicates. Sigali also manipulates cost functions. These are functions that associate to each solution of a predicate a given integer value. These cost functions can be build by associating to each variable a given cost according to the value of the variable.

Starting from the existing functions, it is also possible to define new functions, allowing, from example, to have libraries of functions dedicated to controller synthesis, optimal control or verification. Of course, one can also manipulate ILTS (e.g. to compose them according to different composition operators). Functions allowing to compute the successors (resp. predecessors, etc) belongs to the function kernel of Sigali. They can be further used to implement more intricate functions as the ones that compute the set of reachable states, the set of states that can reach a set of states by triggering uncontrollable events, etc.

For more details regarding Sigali, its syntax and the librairies see the Sigali user manual (pdf)

Sigali front-ends and back-ends

The current implementation of the method relies on the chain of Figure 2. Centrally, we use Sigali, which is a tool that performs model-checking, controller synthesis for logical goals, and optimal controller synthesis.
When the purpose is to control the system, the result of the synthesis in Sigali is a controller, in the form of a logical relation, which can be interpreted by a resolver module: for a given state and uncontrollable inputs, the constraints on controllable signals are solved, for example in an incremental, interactive way following the manual valuation of signals. The resolver can be coupled with the original specification of the uncontrolled system, using either the Polychrony environment, or the tool SigalSimu in the case of Mode Automata.

Distribution

Sigali is freely available for non-commercial use. Download

Note that you will need part of the Polychrony or Matou environment as front-end in order to specify your systems.

Examples

Sigali has been successfully used to verify or control various academics or industrial systems (See the list below).

Papers

More details concerning Sigali are available in the following papers:

haut  

| VerTeCs | Team | Publications | New Results | Softwares |
Irisa - Inria - Copyright 2005 © Projet VerTeCs