An old-fashioned recipe for real time

  • Martín Abadi
  • Leslie Lamport
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 600)


Traditional methods for specifying and reasoning about concurrent systems work for real-time systems. However, two problems arise: the real-time programming version of Zeno's paradox, and circularity in composing real-time assumption/guarantee specifications. Their solutions rest on properties of machine closure and realizability. TLA (the temporal logic of actions) provides a formal framework for the exposition.


Temporal Logic Mutual Exclusion Safety Property Concurrent System Liveness Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Martín Abadi and Leslie Lamport. Composing specifications. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, pages 1–41. Springer-Verlag, May/June 1989.Google Scholar
  2. [2]
    Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82 (2):253–284, May 1991.Google Scholar
  3. [3]
    Martín Abadi and Gordon Plotkin. A logical view of composition and refinement. In Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 323–332, January 1991.Google Scholar
  4. [4]
    Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, October 1985.CrossRefGoogle Scholar
  5. [5]
    Krzysztof R. Apt, Nissim Francez, and Shmuel Katz. Appraising fairness in languages for distributed programming. Distributed Computing, 2:226–241, 1988.CrossRefGoogle Scholar
  6. [6]
    Arthur Bernstein and Paul K. Harter, Jr. Proving real time properties of programs with temporal logic. In Proceedings of the Eighth Symposium on Operating Systems Principles, pages 1–11, New York, 1981. ACM. Operating Systems Review 15, 5.Google Scholar
  7. [7]
    K. Mani Chandy and Jayadev Misra. Parallel Program Design. Addison-Wesley, Reading, Massachusetts, 1988.Google Scholar
  8. [8]
    David L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. PhD thesis, Carnegie Mellon University, February 1988.Google Scholar
  9. [9]
    Leslie Lamport. An assertional correctness proof of a distributed algorithm. Science of Computer Programming, 2(3):175–206, December 1982.CrossRefGoogle Scholar
  10. [10]
    Leslie Lamport. A fast mutual exclusion algorithm. ACM Transactions on Computer Systems, 5(1):1–11, February 1987.CrossRefGoogle Scholar
  11. [11]
    Leslie Lamport. The temporal logic of actions. Technical Report 79, Digital Equipment Corporation, Systems Research Center, 1991. To appear.Google Scholar
  12. [12]
    Keith Marzullo, Fred B. Schneider, and Navin Budhiraja. Derivation of sequential, real-time process-control programs. In Andreé M. van Tilborg and Gary M. Koob, editors, Foundations of Real-Time Computing: Formal Specifications and Methods, chapter 2, pages 39–54. Kluwer Academic Publishers, Boston, Dordrecht, and London, 1991.Google Scholar
  13. [13]
    Peter G. Neumann and Leslie Lamport. Highly dependable distributed systems. Technical report, SRI International, June 1983. Contract Number DAEA18-81-G-0062, SRI Project 4180.Google Scholar
  14. [14]
    Fred B. Schneider, Bard Bloom, and Keith Marzullo. Putting time into proof outlines. This volume.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Martín Abadi
    • 1
  • Leslie Lamport
    • 1
  1. 1.Digital Equipment CorporationPalo AltoUSA

Personalised recommendations