|
|
 |
|
Jeudi 1 Décembre
| Heure: |
15:30 - 16:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Approches pour la modélisation et vérification des systèmes temporisés en utilisant les diagrammes états-transitions et les réseaux de Petri colorés |
| Description: |
Mahdi Benmoussa (Répétition avant soutenance de thèse.)
Nous présentons dans ce travail de thèse des approches pour la spécification et la vérification des systèmes temporisés.
La première partie concerne une méthode de spécification en utilisant les diagrammes états-transitions pour modéliser un système donné en partant d'une description textuelle.
Elle comporte plusieurs étapes et utilise des observateurs d'états et des événements afin d'engendrer le diagramme états-transitions.
Un outil qui implémente les différentes étapes de la méthode de spécification pour une application semi-automatique est présenté.
La seconde partie concerne une traduction des diagrammes états-transitions vers les réseaux de Petri colorés, ce qui permet d'utiliser les méthodes de vérification.
Nous prenons en considération dans cette traduction un ensemble important des éléments syntaxiques des diagrammes états-transitions, tels que la concurrence, la hiérarchie, etc.
Un outil qui implémente la traduction pour un passage automatique des diagrammes états-transitions vers les réseaux de Petri colorés est en cours de développement.
La dernière partie concerne l'intégration des contraintes temporelles dans les deux approches précédentes.
Nous définissons des annotations pour les diagrammes états-transitions dont nous fournissons la syntaxe et la sémantique.
Ces annotations seront ensuite utilisées dans la méthode de spécification et la traduction.
Le but est de proposer des annotations faciles à comprendre et à utiliser avec une syntaxe qui prend en compte des contraintes parmi les plus utilisées. |
|
|
