Specifying and verifying real-time systems using time Petri nets and real-time temporal logic

A method of integrating time predicate transition nets (a class of high-level Petri nets) and real-time first-order temporal logic is developed for specifying and verifying real-time systems. The integration of time predicate transition nets with real-time temporal logic is based on previous work (X. He and J.A.N. Lee, 1990) with the extension of time features so that not only concurrent systems but also real-time systems can be studied in this methodology. The methodology has the following significant features: a real-time system is initially specified by using a time predicate transition net; a consistent real-time temporal logic system (specification) is systematically derived from the time predicate transition net specification; system properties are expressed in real-time temporal logic; and system properties are verified by using the derived real-time temporal logic system with additional pure temporal logic axioms and inference rules. The methodology is illustrated through a simple example.>