Accelerated Simulation of Hybrid Systems : Method combining static analysis and run-time execution analysis.

Ayman Aljarbouh 1
1 HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Résumé : Cette thèse de doctorat porte sur la modélisation et la simulation de systèmes hybrides comportant des phénomènes Zénon. Les systèmes hybrides peuvent être définis comme des systèmes dynamiques dans lesquels les dynamiques en temps continu et les dynamiques en temps discret inter- agissent les unes avec les autres. De tels systèmes existent dans un grand nombre d’applications technologiques où l’évolution de la partie physique du système, le plus souvent modélisée par un système dynamique en temps continu, est combinée avec des actions de contrôle intégrées, modélisée par un système dynamique en temps discret. Les modèles mathématiques des systèmes hybrides consistent généralement en dynamiques de temps continu habituellement décrites par des équations différentielles qui décrivent le comportement continu du système, et des dynamiques d’événements discrets telles que les machines à états finis, qui décrivent le comportement discret du système. Cependant, en raison de l’interaction complexe entre les dynamiques continues et les dynamiques discrètes des systèmes hybrides, les concepteurs des systèmes complexes technologiques devraient accorder une attention particulière lors de la modélisation des systèmes hybrides. En fait, les modèles réalistes de systèmes hybrides nécessitent presque toujours l’abstraction d’une partie du comportement physique du système modélisé. Cette abstraction se fait au moyen d’équations idéales telles que la ré-initialisation et les contraintes conditionnelles qui conduisent généralement à des discontinuités dans les sig- naux physiques du modèle. Le terme abstraction de modélisation est donc désigné pour tout mécanisme qui permet de “cacher” un comportement physique concret en consid- érant des modèles idéalisés. Les modèles ainsi produits peuvent présenter des comporte- ments Zénon, c’est à dire une séquence infinie d’événements discrets se produisant dans un intervalle de temps fini. Fondamentalement, la présence du comportement Zénon indique que le modèle décrive de manière incomplète le comportement physique réel du système hybride. Ce comportement peut être considéré donc comme un problème de modélisation. Nous distinguons deux types de comportement Zénon dans les systèmes hybrides: 1) chattering-Zénon, et 2) genuinely-Zénon. Dans les modèles qui présentent de com- portement chattering-Zénon, le système évolue de façon infinie entre ses états discrets, selon un alternance de transitions de modes et de dynamiques continues différentes à une fréquence infinie. Tout comportement Zénon qui n’est pas chattering-Zénon peut être classifié comme un comportement genuinely-Zénon. Dans cette thèse nous étudions, d’une manière systématique et analytique, le comportement chattering-Zénon et aussi un type particulier de comportement genuinely-Zénon appelé genuinely-Zénon géométrique. Dans les modèles qui présentent de comportement genuinely-Zénon géométrique, une ac- cumulation d’un nombre infini de commutations entre les états discrets — du système hybride — se produit en temps fini. Le comportement genuinely-Zénon géométrique amène la solution du système à converger vers un point limite Zénon selon une série géométrique, c’est à dire, dans les modèles qui présentent de comportement genuinely- Zénon géométrique, les événements discrets se produisent à une période de plus en plus faible, convergeant vers une date limite. La simulation des comportements Zénon — des systèmes hybrides — pose une dif- ficulté majeure: la simulation devient numériquement incorrect; le simulateur devient incapable d’avancer la simulation au delà du point limite Zénon, à cause de l’infinité des commutations discrètes en temps fini. Dans cette thèse, nous considérons les modèles de systèmes hybrides comme des pro- grammes exécutables écrits par des langages de programmation ayant des sémantiques hybrides. Fondamentalement, la définition d’un modèle sémantique hybride approprié est la première étape vers un développement d’un environnement propre de simulation pour les systèmes hybrides. Le développement d’un environnement de simulation hybride consiste généralement à suivre les étapes suivantes: 1. Définir correctement un modèle sémantique hybride, qui peut considérer les pro- priétés de comportement continue/discret des systèmes hybrides. 2. Concevoir et développer un simulateur capable à calculer les dynamiques et les solutions des modèles des systèmes hybrides conformément au modèle sémantique hybride défini. 3. Concevoir et développer un langage de programmation capable d’exprimer tous les éléments et composants des modèles hybrides conformément au modèle sémantique hybride défini. La vérification de code doit être incluse dans cette étape pour prouver de manière statique la validité sémantique des modèles simulés. 4. Concevoir et développer un compilateur pour le langage de programmation développé. Le compilateur devrait être capable d’effectuer une vérification statique efficace des modèles, et rejeter les modèles invalides. De nombreux outils de modélisation et de simulation pour les systèmes hybrides ont été développés ces dernières années. Ils peuvent être classés en deux catégories: ceux qui accordent une attention particulière à une définition rigoureuse des modèles, comme par exemple SpaceEx [44], Ptolemy [27], et Zélus [57], et ceux qui utilisent une approche informelle pour la définition des modèles, comme Simulink 1 , le langage Modelica [55] et ses outils associés. Tous ces outils partagent la même approche de l’exécution du modèle hybride alternant entre l’évolution continue et les séquences de commutations discrètes similaire à l’approche définie par la notion d’automate hybride [30]. Pour tous ces outils, la sémantique opérationnelle de la dynamique continue (équations différen- tielles) n’est pas incluse dans le modèle sémantique: les solveurs numériques exécutent le comportement continu en faisant progresser le temps et en calculant les valeurs des variables continues physiques. Aucun de ces outils n’a un modèle sémantique qui permet de détecter le comportement Zénon et de l’éliminer. Ils comptent tous sur l’analyse de la sortie du solveur à chaque pas d’intégration numérique, sans aucun moyen de spécifier le comportement du solveur au point limite Zénon. Dans cette thèse, nous proposons une solution à ce problème. En particulier, nous proposons une méthode combinant un analyse statique et un analyse à l’execution pour détecter et éliminer le comportement Zénon lors de la simulation des modèles des sys- tèmes hybrides. Nous montrons aussi comment notre méthode peut être utilisée dans le développement d’outils de modélisation et de simulation qui produisent une simulation correcte éliminatoire de comportement Zénon. La première partie de notre contribution est destinée à proposer de sémantique non-standard pour les exécutions Zénon des automates hybrides. Ceci est basé sur l’interprétation des exécutions Zénon dans un domaine de temps hybride non-standard. L’ avantage de l’utilisation de la sémantique non-standard dans l’analyse du comporte- ment Zénon c’est que l’analyse non-standard permet aux solutions des modèles ayant un comportement Zénon d’être bien définies au-delà des points limites Zénon, ainsi que de représenter l’interaction complexe entre les dynamiques continues et les dynamiques discrètes de manière concrète: 1. Les dynamiques continues du système hybride sont réduites à des équations récur- rentes qui représentent rigoureusement l’itération infinie des commutations dis- crètes en durée infinitésimale. Par conséquent, nous pouvons gérer les dynamiques hybrides en appuyant seulement sur un paradigme complètement discret. 2. La représentation non-standard des dynamiques hybrides est complète, qui permet de traiter les points limites Zénon. La deuxième partie de notre contribution est attribuée à proposer une technique de calcul éliminatoire de comportement Zénon. L’idée clé dans notre technique est d’effectuer la détection et l’élimination de comportement Zénon en utilisant l’analyse comportementale du système, au lieu de seulement considérer le nombre des passages à zéro, comme ce qui est le cas désormais dans tous les outils de modélisation et de simu- lation développés pour les systèmes hybrides. La technique d’analyse comportementale que nous proposons pour le traitement de comportement Zénon est basée sur un anal- yse systématique des deux types de Zénon. Nous proposons des conditions formelles pour bien distinguer si les modèles hybrides simulés présentent ou non de comporte- ment Zénon. Nous proposons également des méthodes pour une définition correcte des solutions au delà des points limites Zénon. La question de l’existence et l’unicité de la solution au delà du point limite Zénon est également bien étudiée dans cette thèse. Nos méthodes proposées dans cette thèse permettent de sacrifier la notion de Zénon-free: 1) la décision algorithmique est basé sur des conditions formelles explicitement définies et fournies au simulateur hybride, et 2) la notion correcte de solution au delà du point limite Zénon est bien définie et établie dans notre technique proposée. Des exemples de systèmes hybrides, illustrant l’utilisation des méthodes proposées dans cette thèse, sont également présentés.
Liste complète des métadonnées

https://hal.inria.fr/tel-01614081
Contributeur : Ayman Aljarbouh <>
Soumis le : mardi 10 octobre 2017 - 14:23:20
Dernière modification le : jeudi 12 avril 2018 - 01:55:03

Fichier

Thèse.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : tel-01614081, version 1

Citation

Ayman Aljarbouh. Accelerated Simulation of Hybrid Systems : Method combining static analysis and run-time execution analysis.. Computer Science [cs]. Université de Rennes 1, France, 2017. English. 〈tel-01614081〉

Partager

Métriques

Consultations de la notice

204

Téléchargements de fichiers

133