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.
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.
The various control objectives for which we are able to synthesize a controller
are the following:
- ``Traditional'' control objectives such that:
- the reachability of a set of states from the initial states of the system,
- the attractivity of a set of states E from a set of states F.
- the persistence of a set of states E.
- the reccurence of a set of states E.
- Control objectives expressed as partial order relations over the states
of the system such that:
- the minimally restrictive control (choice of a command such that
the system evolves, at the next instant, into a state where the maximum
number of uncontrollable events is admissible)
- the stabilization of a system (choice of a command such that the
system evolves, at the next instant, into a state with minimal change for the
state variable values)
- the optimal control (minimization of the cost of the trajectories
between a set of initial states and a set of final states)
Sigali front-ends and back-ends
- Sigali is connected with the Polychrony
environment, allowing both the specification of the system in Signal
and the the visualization of the synthesized controller by an interactive
simulation of the controlled system.
- Sigali is now connected with the Matou environment
thus allowing the modeling of reactive systems by means of Mode
Automata. The simulation of the controlled system is also possible.
Distribution
Sigali is freely available for non-commercial use.
Note that you will need part of the Polychrony or Matou environment as
front-end in order to specify your systems.
Papers
More details concerning Sigali are available in the following papers:
- H. Marchand, P. Bournai, M. Le Borgne, P. Le Guernic.
Synthesis of Discrete-Event Controllers based on the Signal Environment. Discrete Event Dynamic System: Theory and Applications, 10(4):325-346, October 2000. (postscript)
- H. Marchand, M. Samaan.
Incremental Design of a Power Transformer Station Controller using Controller Synthesis Methodology. IEEE Transaction on Software Engineering, 26(8):729--741, August 2000. (postscript)
- E. Rutten, H. Marchand.
Task-level programming for control systems using discrete control synthesis. Research report INRIA, No4389, February 2002. (postscript)
- H. Marchand, M. Le Borgne.
The Supervisory Control Problem of Discrete Event Systems using polynomial Methods. Research report Irisa, No1271, October 1999. (postscript)