Interpreted Synchronous Extension of Time Petri Nets - Definition, Semantics and Formal Analysis - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Access content directly
Journal Articles Discrete Event Dynamic Systems Year : 2022

Interpreted Synchronous Extension of Time Petri Nets - Definition, Semantics and Formal Analysis

Hélène Leroux
  • Function : Author
David Andreu

Abstract

Our work is integrated into a global methodology to design synchronously executed embedded critical systems. It is used for the development of medical devices implanted into human body to perform functional electrical stimulation solutions (used in pacemakers, deep brain stimulation...). These systems are of course critical and real time, and the reliability of their behaviors must be guaranteed. These medical devices are implemented into a programmable logic circuit in a synchronous way, which allows efficient implementation (space, consumption and actual parallelism of tasks execution). This paper presents a solution that helps to prove that the behavior of the implemented system respects a set of properties, using Petri nets for modeling and analysis purposes. But one problem in formal methods is that the hardware target and the implementation strategy can have an influence on the execution of the system, but is usually not considered in the modeling and verification processes. Resolving this issue is the goal of this article. Our work has two main results: an operational one, and a theoretical one. First, we can now design critical controllers with hard safety or real time constraints, being sure the behavior is still guaranteed during the execution. Second, this work broadens the scope of expressivity and analyzability of Petri nets extensions. Until then, none managed in the same formalism, both for modeling and analysis, all the characteristics we have considered (weights on arcs, specific test and inhibitor arcs, interpretation, and time intervals, including the management of effective conflicts and the blocking of transitions).
Fichier principal
Vignette du fichier
DISC-S-21-00030_DEDS_VersionFinale.pdf (1.39 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

lirmm-03454630 , version 1 (29-11-2021)

Identifiers

Cite

Karen Godary-Dejean, Hélène Leroux, David Andreu. Interpreted Synchronous Extension of Time Petri Nets - Definition, Semantics and Formal Analysis. Discrete Event Dynamic Systems, 2022, 32, pp.27-64. ⟨10.1007/s10626-021-00347-z⟩. ⟨lirmm-03454630⟩
60 View
134 Download

Altmetric

Share

Gmail Facebook X LinkedIn More