High-level Colored Time Petri Nets for true concurrency modeling in real-time software - Archive ouverte HAL Access content directly
Conference Papers Year :

High-level Colored Time Petri Nets for true concurrency modeling in real-time software

(1, 2) , (2, 1) , (1, 2)
1
2

Abstract

The control of real-time systems often requires taking into account simultaneous access in true parallelism to shared resources. This is particularly the case for multi-core execution platforms. Timed automata or time Petri nets do not capture these features directly. We propose extending time Petri Nets with color and high-level functionality encompassing both timed multi-enableness of transitions and sequential pseudo code. We prove that the reachability problem is decidable for this model on which an on-the-fly TCTL model checking algorithm is efficiently implemented in the tool ROMÉO. We apply this approach to modeling a multi-core real time spinlock mechanism in order to check all possible execution paths and interleaving of service calls.
Fichier principal
Vignette du fichier
codit2022.pdf (235.89 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03872207 , version 1 (25-11-2022)

Identifiers

Cite

Imane Haur, Jean-Luc Béchennec, Olivier Roux. High-level Colored Time Petri Nets for true concurrency modeling in real-time software. 2022 8th International Conference on Control, Decision and Information Technologies (CoDIT), May 2022, Istanbul, Turkey. pp.21-26, ⟨10.1109/CoDIT55151.2022.9803922⟩. ⟨hal-03872207⟩
0 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More