• Jean-Louis FERRIER, Professeur at ISTIA, President
• Janan ZAYTOON, Professeur at Université de Reims Champagne-Ardenne, Reviewer
• Jean-François PETIN, Associate Professor at INPL, Reviewer
• Étienne CRAYE, Professeur à l'École Centrale Lille, Examiner
• Jean-Jacques LESAGE, Professor at ENS Cachan, Supervisor
  
• Jean-Marc ROUSSEL, Associate Professor at ENS Cachan, Co-supervisor

Keywords: algebraic synthesis, logical discrete event system, equations solving on a Boolean algebra

Abstract

The work presented in this memory is relating to the formal development of the control of a logical Discrete Event System (DES) starting from the requirements expressed in the specifications. The method suggested is based on the literal solving of a system of equations representing these requirements.
The mathematical framework, support of this work, is the Boolean algebra of the Boolean functions. This mathematical framework was retained for the following reasons:

• In the particular case of the non temporal logical SED, any control law can be described using Boolean functions.
• The requirements exposed in specifications can be formalized in the form of relations between Boolean functions.
• The results obtained in this thesis enable us to determine automatically which are the Boolean functions which satisfy the system of equations between Boolean functions representing these requirements.
  

The method suggested allows the designer to express the requirements in different formalisms. It also has the possibility of fixing the form of the solution which he wishes to obtain or making the synthesis only on a part of the model.

Chapter 2 of this memory is about the presentation of the mathematical results which we established to be able to solve a system of equations with n unknowns in any structure of Boolean algebra.

The synthesis approach is detailed in chapter 3 through the treatment of 3 examples of increasing size and complexity. We show how the requirements expressed in specifications can be formalized in relations between Boolean functions. The solving of the system of equations is automatically realized with a experimental module developed in the LURPA.