Interpreted Synchronous Extension of Time Petri Nets - Definition, Semantics and Formal Analysis
| العنوان: | Interpreted Synchronous Extension of Time Petri Nets - Definition, Semantics and Formal Analysis |
|---|---|
| المؤلفون: | David Andreu, Karen Godary-Dejean, Helene Leroux |
| المساهمون: | Robotique mobile pour l'exploration de l'environnement (EXPLORE), Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier (LIRMM), Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM), Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM), NEURINNOV |
| المصدر: | Discrete Event Dynamic Systems Discrete Event Dynamic Systems, Springer Verlag, 2021, ⟨10.1007/s10626-021-00347-z⟩ |
| بيانات النشر: | HAL CCSD, 2021. |
| سنة النشر: | 2021 |
| مصطلحات موضوعية: | 0209 industrial biotechnology, Interpretation (logic), Computer science, Distributed computing, Reliability (computer networking), Synchronous Time Petri nets semantics, 0102 computer and information sciences, 02 engineering and technology, Petri net, Formal methods, 01 natural sciences, Blocking (computing), Critical embedded systems, Programmable logic device, Set (abstract data type), [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], 020901 industrial engineering & automation, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, Control and Systems Engineering, Modeling and Simulation, Bisimulation, Electrical and Electronic Engineering, Implementation of Petri nets, Scope (computer science) |
| الوصف: | International audience; 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). |
| اللغة: | English |
| تدمد: | 0924-6703 1573-7594 |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9d787e5995cc561ab7ccf9b24b5a90ed https://hal-lirmm.ccsd.cnrs.fr/lirmm-03454630/document |
| حقوق: | OPEN |
| رقم الأكسشن: | edsair.doi.dedup.....9d787e5995cc561ab7ccf9b24b5a90ed |
| قاعدة البيانات: | OpenAIRE |
Find this article in full text from Springer Verlag. | تدمد: | 09246703 15737594 |
|---|