Garantir la sûreté de fonctionnement d’un système passe généralement
par des vérifications formelles et dynamiques effectuées sur un modèle
du système. Ces méthodes formelles font intervenir des formalismes
complexes, non intuitifs pour un concepteur non spécialiste,
ce qui rend leur utilisation difficile. Ces méthodes sont ainsi pas ou
peu intégrées dans les outils existants de conception de systèmes.
Cet article propose quelques pistes pour appliquer et intégrer des
réseaux de PETRI temporels et d’un outil logiciel dédié, ROMEO, à ces
problématiques de vérification. Ces travaux seront menés dans le cadre
d’une thèse débutant à l’automne 2006, sous financement CIFRE entre la
société Sodius et l’IRCCyN.