Temporal proof methodologies for real-time systems

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.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published | English

Scopus indexed
Author
Henzinger, Thomas AISTA ; Manna, Zohar; Pnueli, Amir
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 ...
Publishing Year
Date Published
1991-01-01
Proceedings Title
Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Publisher
ACM
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.
Page
353 - 366
Conference
POPL: Principles of Programming Languages
Conference Location
Orlando, FL, United States of America
Conference Date
1991-01-21 – 1991-01-23
IST-REx-ID

Cite this

Henzinger TA, Manna Z, Pnueli A. Temporal proof methodologies for real-time systems. In: Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM; 1991:353-366. doi:10.1145/99583.99629
Henzinger, T. A., Manna, Z., & Pnueli, A. (1991). Temporal proof methodologies for real-time systems. In Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 353–366). Orlando, FL, United States of America: ACM. https://doi.org/10.1145/99583.99629
Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “Temporal Proof Methodologies for Real-Time Systems.” In Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 353–66. ACM, 1991. https://doi.org/10.1145/99583.99629.
T. A. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for real-time systems,” in Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Orlando, FL, United States of America, 1991, pp. 353–366.
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.
Henzinger, Thomas A., et al. “Temporal Proof Methodologies for Real-Time Systems.” Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 1991, pp. 353–66, doi:10.1145/99583.99629.

Link(s) to Main File(s)
Access Level
Restricted Closed Access

Export

Marked Publications

Open Data ISTA Research Explorer

Search this title in

Google Scholar
ISBN Search