LPT : Little Parametric Tool, outil pour la validation d'une borne temporelle paramétrée - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Accéder directement au contenu
Communication Dans Un Congrès Année : 2008

LPT : Little Parametric Tool, outil pour la validation d'une borne temporelle paramétrée

Résumé

Cet article s'intéresse au problème de la validation formelle de propriétés temporelles quantitatives et paramétrées pour les systèmes à évènements discrets. Le model checking est une technique d'analyse exhaustive de l'espace des états d'un système modélisé dans un lange formel. Il permet la vérification de propriétés de logique temporelle quantitative. Cependant, l'introduction de paramètres entraine une complexité trop grande de l'analyse, en particulier sur un modèle exprimé en réseaux de Petri temporels. Cet article propose donc une méthode alternative et présente un outil : LPT (Little Parametric Tool) permettant la validation d'une borne temporelle paramétrée. Avec LPT, le modèle du système est analysé et la valeur de la borne maximale est recherchée par l'outil.
Fichier principal
Vignette du fichier
LPT.pdf (111.98 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

lirmm-00330325 , version 1 (14-10-2008)

Identifiants

  • HAL Id : lirmm-00330325 , version 1

Citer

Karen Godary-Dejean. LPT : Little Parametric Tool, outil pour la validation d'une borne temporelle paramétrée. CIFA: Conférence Internationale Francophone d'Automatique, Sep 2008, Bucarest, Roumanie. ⟨lirmm-00330325⟩
125 Consultations
245 Téléchargements

Partager

Gmail Facebook X LinkedIn More