A UNIFIED HIGH-LEVEL PETRI NET FORMALISM FOR TIME-CRITICAL SYSTEMS

Petri nets are a powerful formalism for the specification and analysis of concurrent systems. Thanks to their flexibility, they have been extended and modified in several ways in order to match the requirements of specific application areas. In particular, since Petri nets easily model control flow, some extensions have been proposed to deal with functional aspects while others have taken timing issues into account. Unfortunately, so far little has been done to integrate these aspects, that are crucial in the case of time-critical systems. In this paper, we introduce a high-level Petri net formalism (ER nets) which can be used to specify control, function, and timing issues. In particular, we discuss how time can be modeled via ER nets by providing a suitable axiomatization. Then, we use ER nets to define a time notation (called TB nets), which is shown to generalize most time Petri net-based formalisms which appeared in the literature. Finally, we discuss how ER nets can be used in a specification support environment for time critical system and in particular, the kind of analysis supported.