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 calculation, 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 n-variable 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. This method includes a strategy allowing the proof of consistency of the set of specifications.

It is therefore possible for the designer to propose priority rules between the involved requirements allowing the correction of incoherent specifications.

To avoid tedious symbolic calculus and to help the designer during the different steps of this synthesis method, a prototype software tool has been developed in Python. This tool performs all the computations required for inconsistencies detection and control laws generation. This enables the designer to focus only on application-related issues. For ergonomic reasons, complementary works were also developed in order be able to represent the synthesized control law with a state model.