Advertisement

Formal derivation of CSP programs from temporal specifications

  • Rudolf Berghammer
  • Burghard von Karger
Contributed Lectures
Part of the Lecture Notes in Computer Science book series (LNCS, volume 947)

Abstract

The algebra of relations has been very successful for reasoning about possibly non-deterministic programs, provided their behaviour can be fully characterized by just their initial and final states. We use a slight generalization, called sequential algebra, to extend the scope of relation-algebraic methods to reactive systems, where the behaviour between initiation and termination is also important. To illustrate this approach, we integrate Communicating Sequential Processes and linear temporal logic in sequential algebra and show that the associated calculus permits the formal derivation of CSP programs from temporal specifications.

Keywords

Temporal Logic Linear Temporal Logic Parallel Composition Sequential Calculus Observation Space 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Backhouse R.C., de Bruin P., Malcolm G., Voermans T.S., van der Woude J.: Relational catamorphisms. In: Möller B. (ed.): Constructing programs from specifications. Proceedings IFIP TC2/WG2.1 Working Conference on Constructing Programs, Elsevier Science Publishers, 287–318 (1991)Google Scholar
  2. 2.
    de Bakker J.W., de Roever W.P.: A calculus for recursive program schemes. In: Nivat M. (ed.): Proceedings ICALP 73, North-Holland, 167–196 (1973)Google Scholar
  3. 3.
    Brookes S.D., Roscoe A.W.: An improved failure model for communicating sequential processes. In: Brookes S.D. et al. (eds.): Proceedings NSF-SERC Seminar on Concurrency, LNCS 197, Springer Verlag, 285–305 (1985)Google Scholar
  4. 4.
    Bauer F.L., Möller B., Partsch H., Pepper P.: Formal program construction by transformations — Computer-aided intuition guided programming. IEEE Transactions on Software Engineering 15, 165–180 (1989)Google Scholar
  5. 5.
    Berghammer R., Zierer H.: Relational algebraic semantics of deterministic and nondeterministic programs. Theoretical Computer Science 43, 123–147 (1986)Google Scholar
  6. 6.
    Burstall R.M., Darlington J.: A transformation system for developing recursive programs. Journal of the ACM 24, 44–67 (1977)Google Scholar
  7. 7.
    Chin L.H., Tarski A.: Distributive and modular laws in the arithmetic of relation algebras. University of California Publications in Mathematics (new series) 1, 341–384 (1951)Google Scholar
  8. 8.
    Davies J.: Specification and Proof in Real Time Systems. D. Phil. Thesis, Oxford University (1991)Google Scholar
  9. 9.
    Dijkstra E.W.: The unification of three calculi. In: Broy M. (ed.): Program Design Calculi. Springer Verlag, 197–231 (1993)Google Scholar
  10. 10.
    Goldsmith M.H.: The Oxford occam transformation system (draft user documentation). Oxford University (1994)Google Scholar
  11. 11.
    Goldsmith M.H., Roscoe A.W., Scott B.G.O.: Denotational Semantics for occam 2, parts I & II. Transputer Communications 1(2), 65–91 (1993) and 2(1), 25–67 (1994)Google Scholar
  12. 12.
    Hoare C.A.R.: Communicating Sequential Processes. Prentice-Hall International (1985)Google Scholar
  13. 13.
    Hoare C.A.R., He Jifeng: The weakest prespecification, parts I & II. Fundamenta Informaticae IX, 51–84 & 217–252 (1986)Google Scholar
  14. 14.
    Hoare C.A.R., Roscoe A.W.: The laws of occam programming. Technical Report PRG-53, Oxford University (1986)Google Scholar
  15. 15.
    von Karger B.: Sequential calculus. ProCoS II Report Kiel BvK 15/4, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel (1994)Google Scholar
  16. 16.
    von Karger B.: An algebraic foundation of temporal logic. In: Peter D. Mosses et al. (eds.): Proceedings TAPSOFT '95, LNCS 915, Springer Verlag, 232–246 (1995) Also available as: ProCoS II Report Kiel BvK 17/1, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel (1994)Google Scholar
  17. 17.
    von Karger B., Hoare C.A.R.: Sequential calculus. Information Processing Letters 53, 123–130 (1995)Google Scholar
  18. 18.
    Lamport L., Merz S.: Specifying and verifying fault-tolerant systems. In: Langmaack H. et al. (eds.): Formal techniques in real-time and fault-tolerant systems. LNCS 863, Springer Verlag, 41–76 (1994)Google Scholar
  19. 19.
    Manna Z., Pnueli A.: The temporal logic of reactive and concurrent systems-specification. Springer Verlag (1991)Google Scholar
  20. 20.
    Meertens L.G.L.T: Algorithmics — Towards programming as a mathematically activity. In: de Bakker J.W. et al. (eds.): Proceedings CWI Symposium on Mathematics and Computer Science, CWI Monographs Vol. 1, North Holland, 289–334 (1986)Google Scholar
  21. 21.
    Olderog E.-R., Hoare C.A.R.: Specification-oriented semantics for communicating processes. Acta Informatica 33, 9–66 (1986)Google Scholar
  22. 22.
    Schmidt G.: Programs as partial graphs, parts I & II. Theoretical Computer Science 15, 1–25 & 159–179 (1981)Google Scholar
  23. 23.
    Schmidt G., Ströhlein T.: Relations and graphs. Discrete Mathematics for Computer Scientists, EATCS Monographs on Theoretical Computer Science, Springer Verlag (1993)Google Scholar
  24. 24.
    Spivey J.M.: The Z notation: A reference manual. 2nd ed., Prentice Hall (1992)Google Scholar
  25. 25.
    Tarski A.: On the calculus of relations. Journal of Symbolic Logic 6, 73–89 (1941)Google Scholar
  26. 26.
    Tarski A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285–309 (1955)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Rudolf Berghammer
    • 1
  • Burghard von Karger
    • 1
  1. 1.Institut für Informatik und Praktische MathematikChristian-Albrechts-Universität KielKielGermany

Personalised recommendations