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

He, X. (1991). Specifying and verifying real-time systems using time Petri nets and real-time temporal logic . 135-140.

cited authors

  • He, X

authors

abstract

  • 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.

publication date

  • December 1, 1991

International Standard Book Number (ISBN) 10

start page

  • 135

end page

  • 140