| Autor: |
Libero Nigro, Franco Cicirelli |
| Jazyk: |
angličtina |
| Rok vydání: |
2024 |
| Předmět: |
|
| Zdroj: |
Mathematics, Vol 12, Iss 6, p 812 (2024) |
| Druh dokumentu: |
article |
| ISSN: |
2227-7390 |
| DOI: |
10.3390/math12060812 |
| Popis: |
Modeling and verification of the correct behavior of embedded real-time systems with strict timing constraints is a well-known and important problem. Failing to fulfill a deadline in system operation can have severe consequences in the practical case. This paper proposes an approach to formal modeling and schedulability analysis. A novel extension of Petri Nets named Constraint Time Petri Nets (C-TPN) is developed, which enables the modeling of a collection of interdependent real-time tasks whose execution is constrained by the use of priority and shared resources like processors and memory data. A C-TPN model is reduced to a network of Timed Automata in the context of the popular Uppaal toolbox. Both functional and, most importantly, temporal properties can be assessed by exhaustive model checking and/or statistical model checking based on simulations. This paper first describes and motivates the proposed C-TPN modeling language and its formal semantics. Then, a Uppaal translation is shown. Finally, three models of embedded real-time systems are considered, and their properties are thoroughly verified. |
| Databáze: |
Directory of Open Access Journals |
| Externí odkaz: |
|
|
Nepřihlášeným uživatelům se plný text nezobrazuje |
K zobrazení výsledku je třeba se přihlásit.
|
