Modélisation d'applications temps réel reparties pour la validation de propriétés temporelles méthodologie de construction de modèles et algorithmes de validation - Université de Lorraine Accéder directement au contenu
Thèse Année : 1997

Modeling real time distributed applications to validate time properties design methodology of models and validation algorithms

Modélisation d'applications temps réel reparties pour la validation de propriétés temporelles méthodologie de construction de modèles et algorithmes de validation

Joël Toussaint
  • Fonction : Auteur
  • PersonId : 756520
  • IdRef : 076329461

Résumé

Not available
Ce travail apporte une contribution à la conception d'applications temps réel distribuées validées. Le but essentiel est de garantir des propriétés avant l'implantation, c'est à dire de travailler sur des modèles de l'application. Par applications validées nous entendons vérification que l'application respecte certaines propriétés temporelles. Ces propriétés s'expriment sur des entités communicantes et sont définies sur des événements de modèles de coopération particuliers : client(s)/serveur(s) ou producteur(s)/consommateur(s). Le formalisme de modélisation de l'application qui a été choisi est celui des réseaux de pétri temporels. Nous proposons deux techniques de vérification : vérification directe et vérification par surcharge. La première exploite un graphe d'atteignabilité (le graphe de classes) obtenu à partir du modèle de l'application pour en extraire certains chemins dépendants de la propriété et en analysant ces chemins. La seconde, après avoir surchargé le modèle de l'application d'éléments dépendants de la propriété, consiste à observer le franchissement de certaines transitions particulières sur le graphe d'atteignabilité. Travailler sur des modèles suppose que l'on dispose de tels modèles. Pour construire ces modèles, nous proposons une structuration hiérarchique de l'application en niveaux de service permettant de mettre en évidence les modèles de coopération et la notion de support de communication (qui est le niveau de description que l'on ne désire plus raffiner). Ces modèles et ce support sont représentés et liés entre eux par des interactions en utilisant une approche modulaire. Nous présentons finalement les éléments permettant de construire complètement le modèle de l'application : modules et interactions, méthode support pour leur intégration, quantification au sens temporel du modèle
Fichier non déposé

Dates et versions

tel-01751391 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01751391 , version 1

Accès intranet

Citer

Joël Toussaint. Modélisation d'applications temps réel reparties pour la validation de propriétés temporelles méthodologie de construction de modèles et algorithmes de validation. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 1997. Français. ⟨NNT : 1997INPL114N⟩. ⟨tel-01751391⟩
18 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More