An automated qualitative analysis of real-time systems using Timed Petri net and SPIN

Abstract

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.

Keywords

• Model checking
• formal model
• Timed Petri net
• SPIN
• qualitative analysis
• Dr. Jenhui Chen, Chang Gung University, Taiwan