Maïga, Oumar
[Verfasser:in]
;
Clermont-Ferrand 2
[Mitwirkende:r];
Université des sciences, des techniques et des technologies de Bamako (Mali)
[Mitwirkende:r];
Traoré, Mamadou Kaba
[Mitwirkende:r];
Diallo, Ouaténi
[Mitwirkende:r]
An integrated language for the specification, simulation, formal analysis and enactment of discrete event systems ; Un langage intégré pour la spécification, simulation, analyse formelle et en-action des systèmes à événements discrets
Titel:
An integrated language for the specification, simulation, formal analysis and enactment of discrete event systems ; Un langage intégré pour la spécification, simulation, analyse formelle et en-action des systèmes à événements discrets
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
Cette thèse propose une méthodologie qui intègre les méthodes formelles dans la spécification, la conception, la vérification et la validation des systèmes complexes concurrents et distribués avec une perspective à événements discrets. La méthodologie est basée sur le langage graphique HILLS (High Level Language for System Specification) que nous avons défini. HiLLS intègre des concepts de génie logiciel et de théorie des systèmes pour une spécification des systèmes. Précisément, HiLLS intègre des concepts et notations de DEVS (Discrete Event System Specification), UML (Unified Modeling Language) et Object-Z. Les objectifs de HILLS incluent la définition d’une syntaxe concrète graphique qui facilite la communicabilité des modèles et plusieurs domaines sémantiques pour la simulation, le prototypage, l’enaction et l’accessibilité à l’analyse formelle. L’Enaction se définit par le processus de création d’une instance du système qui s’exécute en temps réel (par opposition au temps virtuel utilisé en simulation). HiLLS permet la construction hiérarchique et modulaire des systèmes à événements discrets grâce à une description simple et rigoureuse des aspects statiques, dynamiques et fonctionnels des modèles. La sémantique pour simulation de HiLLS est définie en établissant un morphisme sémantique entre HiLLS et DEVS; de cette façon chaque modèle HiLLS peut être simulé en utilisant un simulateur DEVS. Cette approche permet aux utilisateurs DEVS d’utiliser HiLLS comme un langage de spécification dans la phase de modélisation et d’utiliser leurs propres implémentations locales ou distribuées de DEVS en phase de simulation. L’enactment des modèles HiLLS est basé sur une adaptation du patron de conception Observateur pour leur implémentation. La vérification formelle est faite en établissant un morphisme entre chaque niveau d’abstraction de HiLLS et une méthode formelle adaptée pour la vérification formelle des propriétés à ce niveau. Les modèles formels sur lesquels sont faites les vérifications formelles sont obtenus à ...