An old-fashioned recipe for real time

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.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, v.82 n.2, p.253-284, May 31, 1991 [doi>10.1016/0304-3975(91)90224-P]
• 2: Martín Abadi , Leslie Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.73-132, Jan. 1993 [doi>10.1145/151646.151649]
• 3: ABADI, M. AND PLOTKIN, G. 1992. A logical view of composition. Research Report 86 (May), Digital Equipment Corporation, Systems Research Center.
• 4: ALPERN, B. AND SCtlNEIDER, F. B. 1985. Defining liveness. Inf. Process. Lett. 21, 4 (Oct.), 181-185.
• 5: APT, K. R., FRANCEZ, N., AND KATZ, S. 1988. Appraising fairness in languages for distributed programming. Distributed Computing 2, 226-241.
• 6: Arthur Bernstein , Paul K. Harter, Jr., Proving real-time properties of programs with temporal logic, Proceedings of the eighth ACM symposium on Operating systems principles, p.1-11, December 14-16, 1981, Pacific Grove, California, United States
• 7: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 8: DE BAKKE1R, J. W., HUIZING, C., DE ROEVElq, \~. P., AND ROZENBERG, (}. (Eds.) 1992. Real- Time: Theory in Practice, Volume 600 of Lecture Notes in Computer Science. Springer- Verlag, Berlin. Proceedings of a REX Real-Time Workshop, held in The Netherlands in June, 1991.
• 9: David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, 1987
• 10: FISCHER, M. 1985. Re: Where are you? E-mail message to Leslie Lamport. Arpanet message sent on June 25, 1985 18:56:29 EDT, number 8506252257.AAO7636@YALE- BULLDOG.YALE.ARPA (47 lines).
• 11: JONES, C. B. 1983. Specification and design of (parallel) programs. In R. E. A. MASON (lEd.), Information Processing 83: Proceedings of the IFIP 9th World Congress, pp. 321-332. IFIP: North-Holland.
• 12: LAMPORT, L. 1982. An assertional correctness proof of a distributed algorithm. Science of Computer Programming 2, 3 (Dec.), 175-206.
• 13: Leslie Lamport, A fast mutual exclusion algorithm, ACM Transactions on Computer Systems (TOCS), v.5 n.1, p.1-11, Feb. 1987 [doi>10.1145/7351.7352]
• 14: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 15: NIARZULLO, K., SCHNEIDER, F. B., AND BUDHIRAJA, N. 1991. Derivation of sequential, real-time process-control programs. In A. M. VAN TILBORG AND Cx. M. KOOB (Eds.), Foundations of Real-Time Computing: Formal Specifications and Methods, Chapter 2, pp. 39-54. Boston, Dordrecht, and London: Kluwer Academic Publishers.
• 16: MISRA, J. AND CHANDY, K. I'~. 1981. Proofa of networks of proceases, lEEK Tya?~sac~iorts 07% ~of~ware Engineering SE-7, 4 (July), 417-426.
• 17: NEUMANN, P. G. AND LAMPORT, L. 1983. Highly dependable distributed systems. Technical report (June), SRI International. Contract Number DAEA18-81-G-0062, SRI Project 4t80.
• 18: A. Pnueli, In transition from global to modular temporal reasoning about programs, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 19: Fred B. Schneider , Bard Bloom , Keith Marzullo, Putting Time into Proof Outlines, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.618-639, June 03-07, 1991

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

General Terms:
Theory, Verification

Keywords:
Zeno, composition, concurrent programming, liveness properties, real time, safety properties, temporal logic