Formal Modeling and Verification of Embedded Real-Time Systems: An Approach and Practical Tool Based on Constraint Time Petri Nets
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 modeli...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2024-03-01
|
| Series: | Mathematics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2227-7390/12/6/812 |
| _version_ | 1797240175681601536 |
|---|---|
| author | Libero Nigro Franco Cicirelli |
| author_facet | Libero Nigro Franco Cicirelli |
| author_sort | Libero Nigro |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-24T18:03:15Z |
| format | Article |
| id | doaj.art-f99bad6a57414dd7a94b7c9e35a8f25e |
| institution | Directory Open Access Journal |
| issn | 2227-7390 |
| language | English |
| last_indexed | 2024-04-24T18:03:15Z |
| publishDate | 2024-03-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Mathematics |
| spelling | doaj.art-f99bad6a57414dd7a94b7c9e35a8f25e2024-03-27T13:52:59ZengMDPI AGMathematics2227-73902024-03-0112681210.3390/math12060812Formal Modeling and Verification of Embedded Real-Time Systems: An Approach and Practical Tool Based on Constraint Time Petri NetsLibero Nigro0Franco Cicirelli1Engineering Department of Informatics Modelling Electronics and Systems Science, University of Calabria, 87036 Rende, ItalyCNR—National Research Council of Italy, Institute for High Performance Computing and Networking (ICAR), 87036 Rende, ItalyModeling 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.https://www.mdpi.com/2227-7390/12/6/812embedded real-time systemstiming constraintsschedulability analysisformal modelinghigh-level time Petri netstimed automata |
| spellingShingle | Libero Nigro Franco Cicirelli Formal Modeling and Verification of Embedded Real-Time Systems: An Approach and Practical Tool Based on Constraint Time Petri Nets Mathematics embedded real-time systems timing constraints schedulability analysis formal modeling high-level time Petri nets timed automata |
| title | Formal Modeling and Verification of Embedded Real-Time Systems: An Approach and Practical Tool Based on Constraint Time Petri Nets |
| title_full | Formal Modeling and Verification of Embedded Real-Time Systems: An Approach and Practical Tool Based on Constraint Time Petri Nets |
| title_fullStr | Formal Modeling and Verification of Embedded Real-Time Systems: An Approach and Practical Tool Based on Constraint Time Petri Nets |
| title_full_unstemmed | Formal Modeling and Verification of Embedded Real-Time Systems: An Approach and Practical Tool Based on Constraint Time Petri Nets |
| title_short | Formal Modeling and Verification of Embedded Real-Time Systems: An Approach and Practical Tool Based on Constraint Time Petri Nets |
| title_sort | formal modeling and verification of embedded real time systems an approach and practical tool based on constraint time petri nets |
| topic | embedded real-time systems timing constraints schedulability analysis formal modeling high-level time Petri nets timed automata |
| url | https://www.mdpi.com/2227-7390/12/6/812 |
| work_keys_str_mv | AT liberonigro formalmodelingandverificationofembeddedrealtimesystemsanapproachandpracticaltoolbasedonconstrainttimepetrinets AT francocicirelli formalmodelingandverificationofembeddedrealtimesystemsanapproachandpracticaltoolbasedonconstrainttimepetrinets |