Contribution à la modélisation réaliste et multi-échelles des systèmes bouclés temporisés

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.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