Real-time programming and asynchronous message passing

ABSTRACT

This paper indicates a method of describing real-time processes and their asynchronous communication by means of message exchanges. This description method is based upon an extension of linear time temporal logic to a special temporal logic in which real-time and asynchronous message passing properties can be expressed. We give a model of this logic, define new operators and show amongst others how they can be applied to specify real-time asynchronous message passing and an abstract real-time transmission medium.

REFERENCES

• 1: "The Programming Language ADA, Reference Manual", Lecture Notes in Computer Science 106, Springer Verlag, New York, 1981.
• 2: Egidio Astesiano , Elena Zucca, Semantics of Distributed Processes Derived by Translation, GI - 11. Jahrestagung in Verbindung mit Third Conference of the European Co-operation in Informatics (ECI), p.78-87, October 20-23, 1981
• 3: 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
• 4: Per Brinch Hansen, Distributed processes: a concurrent programming concept, Communications of the ACM, v.21 n.11, p.934-941, Nov. 1978 [doi>10.1145/359642.359651]
• 5: "CHILL Recommendation Z.200 (CHILL Language Definition)", C.C.I.T.T. Study Group XI, The International Telegraph and Telephone Consultative Committee, Geneva, November 1980.
• 6: Rob Gerth , Willem P. De Roever, A proof system for concurrent ADA programs, Science of Computer Programming, v.4 n.2, p.159-204, August 1984 [doi>10.1016/0167-6423(84)90018-2]
• 7: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 8: Kuiper,R. and de Roever,W.P. "Fairness Assumptions for CSP in a Temporal Logic Framework", TC2 Working Conference on the Formal Description of Programming Concepts, Garmisch, June 1982.
• 9: Lamport,L. "'Sometime' is Sometimes 'NOT Never'", A Tutorial on the Temporal Logic of Programs, SRI International CSL-86, January 1979.
• 10: Zohar Manna , Amir Pnueli, How to cook a temporal proof system for your pet language, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-154, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567082]
• 11: J. Misra , K. M. Chandy , Todd Smith, Proving safety and liveness of communicating processes with examples, Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing, p.201-208, August 18-20, 1982, Ottawa, Canada [doi>10.1145/800220.806698]
• 12: Pnueli,A. and de Roever,W.P. "Rendezvous with ADA - A Proof Theoretical View", Proceedings of the AdaTEC Conference, Crystal City, 1982.
• 13: Schlichting,R.D. and Schneider,F.B. "Using Message Passing for Distributed Programming: Proof Rules and Disciplines", Proceedings of the ACM SIGACT-SIGOPS Conference on the Principles of Distributed Computing, Ottawa, Canada, August 1982.

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.7 COMPUTERS IN OTHER SYSTEMS
      Subjects: Real time

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.4 Communications Management
          Subjects: Message sending

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

General Terms:
Languages