DSC01754.JPG

• Benoit IUNG, Professor at Université de Lorraine, President
• Kamel BARKAOUI, Professor at CNAM, Reviewer
• Audine SUBIAS,  Associate Professor at Université de Toulouse, Reviewer
• Patrice LECLAIRE, Associate Professor at SUPMECA Paris, Examiner
• Jean-Marc FAURE, Professor at SUPMECA Paris, Supervisor
• Jean-François PETIN, Professor at Université de Lorraine, Supervisor
• Patrick SALAUN, Senior research at EDF R&D (STEP), Examiner
  

Abstract
The design of operational control architectures is a very important step of the design of energy production systems. This step consists in mapping the functional architecture of the system onto its hardware architecture while respecting capacity and safety constraints, i.e. in allocating control functions to a set of controllers while respecting these constraints. The work presented in this thesis presents:

• a formalization of the data and constraints of the function allocation problem 
• a mapping method, by reachability analysis, based on a request/response mechanism in a network of communicating automata with integer variables;
• a comparison between this method and a resolution method by integer linear programming.
  

The results of this work have been validated on examples of actual size and open the way to the coupling between reachability analysis and integer linear programming for the resolution of satisfaction problems for non-linear constraint systems.

Keywords
Control architectures, Operational architecture, Communicating automata, Reachability Analysis, Formal Verification