ASC Project

Algebraic Synthesis of Controllers

Leader: Jean-Marc ROUSSEL, Associate Professor.

The strong safety constraints imposed on critical systems lead to advocate the use of formal methods when specifying, designing and implementing the control of these systems.

Given this recommendation, this project is aimed at developing a formal synthesis method for discrete event systems control that allows:

• To provide a formal representation of specifications from statements in natural language,
• To analyze this representation so as to detect specifications inconsistencies and incompleteness,
• To obtain, by symbolic calculus, control laws that comply with the specifications,
• To implement these laws in the form of programs for industrial controllers (Programmable Logic Controllers or real-time controllers).

The formal frame that underlies this method is the Boolean algebra of switching functions. This algebra permits to represent formally the usual specifications of logic discrete event systems (DES) in the form of systems of equations, and to find the solutions of these systems, if any. The absence of solutions points out a specifications inconsistency. Inconsistencies removal is performed by interacting with the designer who must modify the erroneous specifications once inconsistencies detected by symbolic calculus. The other steps of the method are fully automated.