An automated qualitative analysis of real-time systems using Timed Petri net and SPIN
| Autor: | Tanuja Shailesh, Ashalatha Nayak, Devi Prasad |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2024 |
| Předmět: | |
| Zdroj: | Cogent Engineering, Vol 11, Iss 1 (2024) |
| Druh dokumentu: | article |
| ISSN: | 23311916 2331-1916 |
| DOI: | 10.1080/23311916.2024.2375100 |
| Popis: | Verification of real-time system properties using formal models can improve system design and quality. The Timed Petri net is a formal model for modelling and designing real-time systems with time constraints. Furthermore, model checking is a formal verification method used to verify system properties using model checkers. This article proposes an automated transformation system for mapping a Timed Petri net into one of the common model checkers, the SPIN PROMELA model, to verify real-time system properties. This approach enables the combination of two modelling paradigms and supports system verification using system design models. In this study, the system properties were verified using both the simulation method and linear temporal logic formulas supported by the SPIN model checker. Timed Petri net models of two different case studies, a central server computer system and a manufacturing Kanban system were considered to verify the boundedness, liveness and system behavioral properties using the proposed transformation system. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|