LogoLogo

Boudjadar, Abdeldjalil. Sémantique compositionnelle et raffinement de systèmes temporisés : application aux automates temporisés d'UPPAAL et au langage FIACRE

Boudjadar, Abdeldjalil (2012). Sémantique compositionnelle et raffinement de systèmes temporisés : application aux automates temporisés d'UPPAAL et au langage FIACRE.

[img]
Preview
PDF - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
1983Kb

Résumé en francais

Les systèmes temps-réel sont massivement impliqués dans de nombreuses applications, dont notre vie dépend comme les logiciels embarqués dans les voitures et les avions. Pour ces systèmes des erreurs inattendues ne sont pas acceptables. De ce fait, assurer la correction de ces systèmes est une tâche primordiale. Les systèmes temps-réel représentent un large spectre de systèmes automatisés dont la correction dépend de la ponctualité des événements (timeliness) et pas seulement de leurs propriétés fonctionnelles. Chaque événement doit être produit selon la date indiquée par la spécification du système. Les systèmes temps-réel sont concurrents et embarqués, et conçus comme un assemblage de composants en interaction. Malgré les progrès réalisés dans les techniques de model checking, la vérification et l'analyse des systèmes temps-réel représentent toujours un défi autant pour les chercheurs que les praticiens. Pour étudier le comportement des systèmes temps-réel, différents formalismes ont été considérés comme les automates temporisés, les réseaux de Petri temporisés et les algèbres de processus. Cela donne lieu à plusieurs points délicats concernant le raffinement, la composition et la vérification. Ces points représentent un champ de recherche intensif. Ma thèse présente une étude des systèmes temps-réel focalisée sur les notions de sémantique, de composition et de raffinement. Elle décrit nos efforts pour explorer et étendre les formalismes temps-réel. Nous avons abordé les concepts de base de la modélisation des systèmes temps réel tels que les variables partagées, la communication, les priorités, la dynamicité, etc. La contribution de cette thèse porte sur la définition d’un cadre formel pour raisonner sur la sémantique, la composition et le raffinement des systèmes temporisés. Nous avons instancié ce cadre pour le formalisme des automates temporisés et le langage Fiacre.

Sous la direction du :
Directeur de thèse
Bodeveix, Jean-Paul
Filali, Mamoun
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :Systèmes temporisés - Sémantique - Composition - Raffinement - Uppaal - Automates temporisés - Langage Fiacre
Sujets :Informatique
Déposé le :22 Apr 2013 15:02