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 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: (1) a real-time system is initially specified by using a time predicate transition net, (2) a consistent real-time temporal logic system (specification) is systematically derived from the time predicate transition net specification, (3) system properties are expressed in real-time temporal logic, and (4) 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.
