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)