Spécification et Vérification des Propriétés Temporelles Qualitatives et Quantitatives des Systèmes Temps Réel Complexes

Résumé

L’analyse et la vérification des systèmes temps réels complexes permettent de répondre aux questions liées, essentiellement, à la fiabilité et à la sûreté de fonctionnement de ces derniers. En effet, le ModelCheking : vérification du/sur le modèle, est une méthode très connue permettant de vérifier les propriétés qualitatives (e.g : accessibilité d’un état, vivacité, bloquage, etc...) et/ou quantitatives (e.g : la réponse du temps borné) sur le modèle. Le formalisme des réseaux de Petri et ses extensions sont largement utilisés dans la littérature, offrant un nombre considérables d’avantages citons : (sa représentation graphique et intuitive, ses techniques abondantes d’analyses...etc.). Nous nous intéressons aux réseaux de Petri comme outil de modélisation, étendu au temps et aux mécanismes de synchronisation. En conséquence, une nouvelle extension du modèle de base est proposée notée RT P N pour : (Time Petri Nets with Rendezvous). Ensuite, nous proposons une sous-classe du modèle proposé, noté RTW F N pour : (Time Workflow Nets with Rendezvous) dédiée aux réseaux de Workflows. Une méthode d’abstraction de l’espace d’états (généralement infini ) du modèle est proposée par la suite. La méthode consiste à regrouper un ensemble d’états partageant les même propriétés et basé sur le formalisme de classe d’état. Enfin, l’analyse et la vérification des propriétés qualitatives et quantitatives sur le modèle ,et bien évidement, sur le système en question devient possibles.

Citer ce document

Accès au document

Ce document est hébergé sur son dépôt institutionnel d'origine.

Auteur(s)

Statistiques

Consultations : 3

Téléchargements : 0