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

Karen Godary-Dejean 1
1 EXPLORE - Robotique mobile pour l'exploration de l'environnement
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
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.
Complete list of metadatas

Cited literature [2 references]  Display  Hide  Download

https://hal-lirmm.ccsd.cnrs.fr/lirmm-00330325
Contributor : Karen Godary-Dejean <>
Submitted on : Tuesday, October 14, 2008 - 10:47:16 AM
Last modification on : Thursday, February 14, 2019 - 8:44:01 AM
Long-term archiving on: Monday, June 7, 2010 - 5:55:24 PM

File

LPT.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : lirmm-00330325, version 1

Citation

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⟩

Share

Metrics

Record views

205

Files downloads

256