LPT - A Tool for Parametric TPN Validation

Karen Godary-Dejean 1 Romain Richard 2 Gregory Angles 3 David Andreu 3
1 EXPLORE - Robotique mobile pour l'exploration de l'environnement
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
2 LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
3 DEMAR - Artificial movement and gait restoration
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier, CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This article deals with the problem of temporal and parametric formal validation for discrete event systems. It particularly focuses on the time Petri nets formalism, for which the parametric property verification with model checking is still a non resolved problem. A method is proposed, combining no parametric timed model checking with classical iterative algorithms to avoid combinatory explosion of the analysis process. Algorithms are proposed for the verification of several property types into two specific hypothesis, depending on the parameters values. They have been implemented into a tool: LPT (Little Parametric Tool), which has been used to validate a buffer management system to illustrate the given method.
Keywords : Parametric formal validation Model checking verification Time Petri Nets
Type de document :
Communication dans un congrès
VECoS: Verification and Evaluation of Computer and Communication Systems, Aug 2012, Paris, France. 6th International Workshop on Verification and Evaluation of Computer and Communication Systems, 2012, 〈vecos.ensta-paristech.fr/2012/〉
Liste complète des métadonnées
https://hal-lirmm.ccsd.cnrs.fr/lirmm-00804362
Contributeur : Karen Godary-Dejean <>
Soumis le : lundi 25 mars 2013 - 14:06:52
Dernière modification le : jeudi 24 mai 2018 - 15:59:23
Document(s) archivé(s) le : dimanche 2 avril 2017 - 19:58:19

Fichier

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

Identifiants

  • HAL Id : lirmm-00804362, version 1

Collections

INRIA | EXPLORE | DEMAR | LIRMM | MIPS | UNIV-MONTPELLIER

Citation

Karen Godary-Dejean, Romain Richard, Gregory Angles, David Andreu. LPT - A Tool for Parametric TPN Validation. VECoS: Verification and Evaluation of Computer and Communication Systems, Aug 2012, Paris, France. 6th International Workshop on Verification and Evaluation of Computer and Communication Systems, 2012, 〈vecos.ensta-paristech.fr/2012/〉. 〈lirmm-00804362〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

366

Téléchargements de fichiers

395

Contact

support.ccsd.cnrs.fr
hal.support@ccsd.cnrs.fr
Logo CCSD