An Efficient Approach for Model-Checking Zeno Behaviors in Real-Time System Models Based on the Time Petri Net Formalism

This work focuses on Real-time system models based on the Time Petri Net (TPN) formalism and addresses a pathological aspect known to often affect models of Real-Time Systems called Zeno Behavior or Zenoness. Zenoness permits a system’s model to perform an unbounded number of actions in a finite amount of time, which violates a fundamental requirement for real-time systems that they can’t be infinitely fast. To verify Zenoness on TPNs, the only known technique requires translating a TPN into an equivalent timed automaton, then performing the test on the translation, losing in the process performance and the ease of interpreting the results back and forth between the original model and its translation. In this work, we propose an efficient approach to model-check Zenoness directly on the TPN model. We start by stating a necessary and sufficient condition for TPNs to be Zeno, then derive some interesting structural properties regarding Zenoness and an efficient algorithm to model-check Zenoness for bounded TPNs. Our results provide a good insight into how to avoid Zenoness during design time, how to spot the problem when it occurs, and how to rectify it. Note to Practitioners—When designing a Real-time system for critical industrial applications, we are often required to model the system using some mathematical formalism. The objective is to formally verify that our design meets some important functional and non-functional requirements when it is implemented. Mathematical formalisms such as Timed Automata (TA) and timed extensions of Petri Nets are often used for that purpose. One of these extensions called Time Petri Net (TPN) is known to be intuitive and simple, yet very versatile and powerful. When creating a model for a Real-time system, one critical aspect called Zenoness is often neglected or unforeseen. Zenoness is a modeling flaw that can easily be unintentionally injected during the modeling phase of a Real-time system but is often very difficult to spot. A model is Zeno if it can perform infinitely many actions in a finite amount of time. Although this behavior is unrealistic for Real-time systems, it can lead to false conclusions during the verification process of the model and catastrophic implications for the implemented system. An approach has been developed to verify Zenoness for the TA formalism, but no method exists yet to verify Zenoness directly on TPNs. In this work, we show how to efficiently verify Zenoness directly on the TPN formalism, and provide some useful insights into how to minimize the risk of unintentionally injecting Zenoness in a TPN model during design time.