Matthieu PERIN

• Etienne CRAYE, Professor at Ecole Centrale de Lille, President
• Eric NIEL, Professor at INSA de Lyon, Reviewer
  
• Eric RUTTEN , Researcher (HdR) at INRIA Grenoble, Reviewer
• Alexandre PHILIPOT, Associate Professor at université de Reims Champagne-ardenne, Examiner
  
• Jean-Marc FAURE, Professor at SupMéca, Thesis supervisor
• François BICHET, Senior engineer at Dassault Systèmes, Industrial guest

Keywords

Equivalent models - Systems patterns - Temporized models

Abstract
The analysis of a complete industrial production line, composed of several closed-loop systems, using detailed models is almost impossible due to size-related issues. A solution consists in performing a multi-scale analysis which uses some abstract models in place of detailed ones. In order to guarantee the analysis result, the detailed models need to have a correct behavior, and the abstract model of a closed-loop system has to be equivalent to the detailed model of the same closed-loop system.

The first contribution details the construction process and the solutions used to build a correct --exempt from unrealistic evolutions-- model of a timed closed-loop system. This is achieved by using an urgency semantics upon timed automata with synchronization variables.

The second contribution consists in proposing an equivalence which is suitable for the multi-scale analysis and then in proposing a technique --using formal methods-- to prove the equivalence between the abstract and detailed models.