An old-fashioned recipe for real time

1 September 1994

journal article
Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems

Vol. 16 (5) , 1543-1571
https://doi.org/10.1145/186025.186058

Abstract

Traditional methods for specifying and reasoning about concurrent systems work for real-time systems. Using TLA (the temporal logic of actions), we illustrate how they work with the examples of a queue and of a mutual-exclusion protocol. In general, two problems must be addressed: avoiding the real-time programming version of Zeno's paradox, and coping with circularities when composing real-time assumption/guarantee specifications. Their solutions rest on properties of machine closure and realizability.

Keywords

This publication has 9 references indexed in Scilit:

The temporal logic of actions
ACM Transactions on Programming Languages and Systems, 1994
Composing specifications
ACM Transactions on Programming Languages and Systems, 1993
The existence of refinement mappings
Theoretical Computer Science, 1991
Appraising fairness in languages for distributed programming
Distributed Computing, 1988
A fast mutual exclusion algorithm
ACM Transactions on Computer Systems, 1987
Defining liveness
Information Processing Letters, 1985
In Transition From Global to Modular Temporal Reasoning about Programs
Published by Springer Nature ,1985
An assertional correctness proof of a distributed algorithm
Science of Computer Programming, 1982
Proofs of Networks of Processes
IEEE Transactions on Software Engineering, 1981