Integrating Implementation Properties in Analysis of Petri Nets Handling Exceptions

Hélène Leroux 1 Karen Godary-Dejean 2 David Andreu 1, 2
1 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
2 EXPLORE - Robotique mobile pour l'exploration de l'environnement
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
Abstract : To design and implement complex digital systems, designers need to have an efficient methodology. In this goal, HILECOP has been developed to transform automatically Petri nets in a VHDL code. To ease design and increase the reactivity of exception handling, the mechanism of macroplace has been added to the formalism of Petri nets. This article describes an automatic model transformation for the analysis step. It integrates implementation properties to enhance reliability.
Keywords : Discrete-event systems Formal verification Exception Petri-nets Implementation
Document type :
Journal articles
Complete list of metadatas
https://hal-lirmm.ccsd.cnrs.fr/lirmm-01064146
Contributor : Karen Godary-Dejean <>
Submitted on : Tuesday, May 21, 2019 - 2:13:46 PM
Last modification on : Tuesday, May 21, 2019 - 2:56:19 PM

File

1-s2.0-S1474667015374358-main....
Publisher files allowed on an open archive

Identifiers

Collections

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

Citation

Hélène Leroux, Karen Godary-Dejean, David Andreu. Integrating Implementation Properties in Analysis of Petri Nets Handling Exceptions. IFAC Proceedings Volumes, Elsevier, 2014, 12th IFAC International Workshop on Discrete Event Systems (WODES), 47 (2), pp.406-411. ⟨10.3182/20140514-3-FR-4046.00032⟩. ⟨lirmm-01064146⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

306

Files downloads

11

Contact

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