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.
Type de document :
Communication dans un congrès
CIFA: Conférence Internationale Francophone d'Automatique, Sep 2008, Bucarest, Roumanie. 2008
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger

https://hal-lirmm.ccsd.cnrs.fr/lirmm-00330325
Contributeur : Karen Godary-Dejean <>
Soumis le : mardi 14 octobre 2008 - 10:47:16
Dernière modification le : jeudi 11 janvier 2018 - 06:26:17
Document(s) archivé(s) le : lundi 7 juin 2010 - 17:55:24

Fichier

LPT.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. 2008. 〈lirmm-00330325〉

Partager

Métriques

Consultations de la notice

158

Téléchargements de fichiers

228