@inproceedings{4508,
  abstract     = {We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of concurrent and reactive systems. A global, discrete, and asynchronous clock is incorporated into the model by defining the abstract notion of a real-time transition system as a conservative extension of traditional transition systems: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upperbound real-time requirements for transitions. We show how to model real-time systems that communicate either through shared variables or by message passing, and how to represent the important real-time constructs of priorities (interrupts), scheduling, and timeouts in this framework. Two styles for the specification of real-time properties are presented. The first style uses bounded versions of the temporal operators; the real-time requirements expressed in this style are classified ...},
  author       = {Henzinger, Thomas A and Manna, Zohar and Pnueli, Amir},
  booktitle    = {Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  isbn         = {978-0-89791-419-2},
  location     = {Orlando, FL, United States of America},
  pages        = {353 -- 366},
  publisher    = {ACM},
  title        = {{Temporal proof methodologies for real-time systems}},
  doi          = {10.1145/99583.99629},
  year         = {1991},
}