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
Conference Papers Year : 2008

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

Abstract

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
Origin Files produced by the author(s)
Loading...

Dates and versions

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

Identifiers

  • HAL Id : lirmm-00330325 , version 1

Cite

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⟩
129 View
254 Download

Share

More