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
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.
Complete list of metadatas

https://hal-lirmm.ccsd.cnrs.fr/lirmm-00804362
Contributor : Karen Godary-Dejean <>
Submitted on : Monday, March 25, 2013 - 2:06:52 PM
Last modification on : Thursday, February 14, 2019 - 8:44:01 AM
Long-term archiving on: Sunday, April 2, 2017 - 7:58:19 PM

File

VECoS12_GodaryDejean.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : lirmm-00804362, version 1

Collections

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. ⟨lirmm-00804362⟩

Share

Metrics

Record views

440

Files downloads

577