Résumé du séminaire du 30 Mars 2004


Jérôme DELATOUR - Graphe de classe et logique linéaire pour la vérification de contraintes temporelles.

Dans le cadre de la définition de l'approche UML/PNO (Unified Modelling Language with Petri Net Objects) pour la spécification de systèmes temps réel, nous avons travaillé (équipe OCSD du LAAS et Trame de l'ESEO) sur la vérification des contraintes temporelles.

Cette vérification utilise les techniques d'analyse formelle, basées sur l'utilisation conjointe du graphe de classes et de la logique linéaire. Une approche de vérification quantitative des contraintes temporelles est proposée au niveau de l'analyse des besoins et des exigences du système.

Après une présentation de cette approche de vérification, nous présenterons les problèmes auxquels nous sommes maintenant confrontés. L'objectif de cette présentation est d'identifier des coopérations possibles entre l'équipe TRAME de l'ESEO et le LISA. Nous espérons, en effet, que des compétences du LISA, par exemple celles sur les solveurs de contraintes ou l'approche Min/Max, pourraient nous aider dans la résolution de nos problèmes.

Mots-clefs: UML temps réel, Réseaux de Petri, contraintes temporelles, analyse des besoins, spécification, validation et vérification.