---
_id: '4510'
abstract:
- lang: eng
  text: "The interleaving model is both adequate and sufficiently abstract to allow
    for the practical specification and verification of many properties of concurrent
    systems. We incorporate real time into this 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 upper-bound real-time requirements for transitions.\r\nWe present
    proof rules to establish lower and upper real-time bounds for response properties
    of real-time transition systems. This proof system can be used to verify bounded-invariance
    and bounded-response properties, such as timely termination of shared-variables
    multi-process systems, whose semantics is defined in terms of real-time transition
    systems."
acknowledgement: 'Sponsors: IBM graduate fellowship,  National Science Foundation
  grant CCR-89-11512,  National Science Foundation CCR-89-13641, Defense Advanced
  Research Projects Agency under contract N00039-84-C-0211,  United States Air Force
  Office of Scientific Research under contract AFOSR-90-0057,  European Community
  ESPRIT Basic Research Action project 3096 (SPEC).'
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. An interleaving model for real time. In:
    <i> Proceedings of the 5th Jerusalem Conference on Information Technology</i>.
    IEEE; 1990:717-730. doi:<a href="https://doi.org/10.1109/JCIT.1990.128356">10.1109/JCIT.1990.128356</a>'
  apa: 'Henzinger, T. A., Manna, Z., &#38; Pnueli, A. (1990). An interleaving model
    for real time. In <i> Proceedings of the 5th Jerusalem Conference on Information
    Technology</i> (pp. 717–730). Jerusalem, Israel: IEEE. <a href="https://doi.org/10.1109/JCIT.1990.128356">https://doi.org/10.1109/JCIT.1990.128356</a>'
  chicago: Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “An Interleaving Model
    for Real Time.” In <i> Proceedings of the 5th Jerusalem Conference on Information
    Technology</i>, 717–30. IEEE, 1990. <a href="https://doi.org/10.1109/JCIT.1990.128356">https://doi.org/10.1109/JCIT.1990.128356</a>.
  ieee: T. A. Henzinger, Z. Manna, and A. Pnueli, “An interleaving model for real
    time,” in <i> Proceedings of the 5th Jerusalem Conference on Information Technology</i>,
    Jerusalem, Israel, 1990, pp. 717–730.
  ista: 'Henzinger TA, Manna Z, Pnueli A. 1990. An interleaving model for real time.  Proceedings
    of the 5th Jerusalem Conference on Information Technology. JCIT: Jerusalem Conference
    on Information Technology, 717–730.'
  mla: Henzinger, Thomas A., et al. “An Interleaving Model for Real Time.” <i> Proceedings
    of the 5th Jerusalem Conference on Information Technology</i>, IEEE, 1990, pp.
    717–30, doi:<a href="https://doi.org/10.1109/JCIT.1990.128356">10.1109/JCIT.1990.128356</a>.
  short: T.A. Henzinger, Z. Manna, A. Pnueli, in:,  Proceedings of the 5th Jerusalem
    Conference on Information Technology, IEEE, 1990, pp. 717–730.
conference:
  end_date: 1990-10-25
  location: Jerusalem, Israel
  name: 'JCIT: Jerusalem Conference on Information Technology'
  start_date: 1990-10-22
date_created: 2018-12-11T12:09:14Z
date_published: 1990-01-01T00:00:00Z
date_updated: 2022-02-15T15:51:25Z
day: '01'
doi: 10.1109/JCIT.1990.128356
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://ieeexplore.ieee.org/abstract/document/128356
month: '01'
oa_version: None
page: 717 - 730
publication: ' Proceedings of the 5th Jerusalem Conference on Information Technology'
publication_identifier:
  isbn:
  - 0-8186-2078-1
publication_status: published
publisher: IEEE
publist_id: '220'
quality_controlled: '1'
scopus_import: '1'
status: public
title: An interleaving model for real time
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1990'
...