High-level Colored Time Petri Nets for true concurrency modeling in real-time software - l'unam - université nantes angers le mans Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

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

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Identifiants

Citer

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⟩
13 Consultations
69 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More