---
_id: '4508'
abstract:
- lang: eng
  text: '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 ...'
acknowledgement: 'This research was supported in part by an IBM graduate fellowship,
  by the National Science Foundation grants CCR-89-11512 and CC R-89-13641, by the
  Defense Advanced Re-search Projects Agency under contract NOO03%84C-0211, by the
  United States Air Force Office of Scientific Research un-der contract AFOSR-W-0057,
  and by the European Community ESPRIT Basic Research Action project 3096 (SPEC).
  We thank Rajeev Alur for many helpful discussions. '
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Zohar
  full_name: Manna, Zohar
  last_name: Manna
- first_name: Amir
  full_name: Pnueli, Amir
  last_name: Pnueli
citation:
  ama: 'Henzinger TA, Manna Z, Pnueli A. Temporal proof methodologies for real-time
    systems. In: <i>Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles
    of Programming Languages</i>. ACM; 1991:353-366. doi:<a href="https://doi.org/10.1145/99583.99629">10.1145/99583.99629</a>'
  apa: 'Henzinger, T. A., Manna, Z., &#38; Pnueli, A. (1991). Temporal proof methodologies
    for real-time systems. In <i>Proceedings of the 18th ACM SIGPLAN-SIGACT symposium
    on Principles of programming languages</i> (pp. 353–366). Orlando, FL, United
    States of America: ACM. <a href="https://doi.org/10.1145/99583.99629">https://doi.org/10.1145/99583.99629</a>'
  chicago: Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “Temporal Proof Methodologies
    for Real-Time Systems.” In <i>Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium
    on Principles of Programming Languages</i>, 353–66. ACM, 1991. <a href="https://doi.org/10.1145/99583.99629">https://doi.org/10.1145/99583.99629</a>.
  ieee: T. A. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for
    real-time systems,” in <i>Proceedings of the 18th ACM SIGPLAN-SIGACT symposium
    on Principles of programming languages</i>, Orlando, FL, United States of America,
    1991, pp. 353–366.
  ista: 'Henzinger TA, Manna Z, Pnueli A. 1991. Temporal proof methodologies for real-time
    systems. Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of
    programming languages. POPL: Principles of Programming Languages, 353–366.'
  mla: Henzinger, Thomas A., et al. “Temporal Proof Methodologies for Real-Time Systems.”
    <i>Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
    Languages</i>, ACM, 1991, pp. 353–66, doi:<a href="https://doi.org/10.1145/99583.99629">10.1145/99583.99629</a>.
  short: T.A. Henzinger, Z. Manna, A. Pnueli, in:, Proceedings of the 18th ACM SIGPLAN-SIGACT
    Symposium on Principles of Programming Languages, ACM, 1991, pp. 353–366.
conference:
  end_date: 1991-01-23
  location: Orlando, FL, United States of America
  name: 'POPL: Principles of Programming Languages'
  start_date: 1991-01-21
date_created: 2018-12-11T12:09:13Z
date_published: 1991-01-01T00:00:00Z
date_updated: 2022-02-24T14:44:39Z
day: '01'
doi: 10.1145/99583.99629
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://dl.acm.org/doi/10.1145/99583.99629
month: '01'
oa_version: None
page: 353 - 366
publication: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of
  programming languages
publication_identifier:
  isbn:
  - 978-0-89791-419-2
publication_status: published
publisher: ACM
publist_id: '221'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Temporal proof methodologies for real-time systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1991'
...