Matthieu PERIN

• Etienne CRAYE, Professeur à l'Ecole Centrale de Lille, Président
• Eric NIEL, Professeur à l'INSA de Lyon, Rapporteur
  
• Eric RUTTEN, Chargé de Recherche (HdR) à l'INRIA Grenoble, Rapporteur
• Alexandre PHILIPOT,Maître de Conférences à l'université de Reims Champagne-ardenne, Examinateur
  
• Jean-Marc FAURE, Professeur à SupMéca (Institut supérieur de Mécanique de Paris), Directeur de thèse
• François BICHET, Ingénieur senior à Dassault Systèmes, Invité industriel

Mots-clés

Équivalence de modèles - Modèles de systèmes bouclés - Modèles temporisés.

Résumé

L'analyse d'une chaîne de production manufacturière complète, composée de plusieurs systèmes bouclés temporisés, en utilisant des modèles détaillés est presque impossible à cause des problèmes liés aux tailles des modèles. Une solution pour contourner ces difficultés consiste à utiliser des techniques d'analyse multi-échelles utilisant à la fois des modèles détaillés des système bouclés, lorsque nécessaire, mais aussi des modèles abstraits de certains systèmes bouclés dès que possible.

Afin de garantir les résultats lors d'analyses multi-échelles, il convient de garantir que les modèles détaillés des systèmes bouclés ne permettent pas d'évolutions indésirables ne représentant pas un comportement réaliste des système bouclés, et que les modèles abstraits des système bouclés utilisés pendant l'analyse ont un comportement identique aux modèles détaillés de ces mêmes systèmes bouclés.

La première contribution de ces travaux est une méthodologie de conception de modèles détaillés, utilisant des automates temporisés, de systèmes bouclés temporisés permettant de supprimer les évolutions irréalistes. Les solutions proposées pour y parvenir se basent sur une conception modulaire, des mécanismes d'urgence et des variables partagées.

La seconde contribution de ces travaux est axée sur la vérification de l'équivalence entre les modèles détaillé et abstrait d'un même système bouclé. Pour ce faire, une équivalence conforme aux exigences d'une analyse multi-échelles est retenue, puis une méthode basée sur un automate observateur-séquenceur couplé à un model-checker est décrite. Enfin, la prise en compte d'une équivalence avec tolérances (en valeur et/ou temporelle) est détaillée.