Skip to main content
SpringerLink
Log in

Systematic Derivation of Communicating Programs

  • Conference paper
Programming and Mathematical Method

Part of the book series: NATO ASI Series ((NATO ASI F,volume 88))

  • 86 Accesses

Abstract

We present an approach to the top-down derivation of communicating, concurrent programs from their specification. As a programming language we use a blend of Milner’s CCS, Hoare’s CSP and Lauer’s COSY, and as a specification language we use a version of Zwiers’ trace logic. The link between communicating programs and trace specifications is given by a notion of program correctness which deals with both safety and liveness properties. The top-down derivation proceeds by application of compositional transformation rules which refine the given trace specification stepwise into a communicating program satisfying the safety and liveness requirements of the specification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. F. André, D. Herman, J.-P. Verjus, Synchronization of Parallel Programs (MIT Press, Cambridge, Mass., 1985).

    MATH  Google Scholar 

  2. B. Alpern, F.B. Schneider, Defining liveness, Inform. Proc. Letters 21 (1985) 181–185.

    Article  MATH  MathSciNet  Google Scholar 

  3. J.W. de Bakker, Mathematical Theory of Program Correctness (Prentice-Hall, London, 1989).

    Google Scholar 

  4. F.L. Bauer et al, The Munich Project CIP, Vol. I: The Wide Spectrum Language CIP-L, Lecture Notes in Comput. Sci. 183 (Springer-Verlag, 1985).

    Google Scholar 

  5. F.L. Bauer et al., The Munich Project CIP, Vol. II: The Program Transformation System CIP-S, Lecture Notes in Comput. Sci. 292 (Springer-Verlag, 1987).

    Google Scholar 

  6. E. Best, COSY: its relation to nets and CSP, in: W. Brauer, W. Reisig, G. Ro-zenberg (Eds.), Petri Nets: Applications and Relationships to Other Models of Concurrency, Lecture Notes in Comput. Sci. 255 ( Springer-Verlag, 1987) 416–440.

    Google Scholar 

  7. S.D. Brookes, C.A.R. Hoare, A.W. Roscoe, A theory of communicating sequen tial processes, J. ACM 31 (1984) 560–599.

    Article  MATH  MathSciNet  Google Scholar 

  8. Z. Chaochen, C.A.R. Hoare, Partial correctness of communicating processes, in: Proc. 2nd Intern. Conf. on Distributed Comput. Systems, Paris, 1981.

    Google Scholar 

  9. R. DeNicola, M. Hennessy, Testing equivalences for processes, Theoret. Comput. Sci. 34 (1984) 83–134.

    Article  MathSciNet  Google Scholar 

  10. E.W. Dijkstra, A Discipline of Programming ( Prentice-Hall, Englewood Cliffs, NJ, 1976).

    MATH  Google Scholar 

  11. N. Francez, D. Lehmann, A. Pnueli, A linear history semantics for languages for distributed programmming, Theoret. Comput. Sci. 32 (1984) 25–46.

    Article  MATH  MathSciNet  Google Scholar 

  12. U. Goltz, Über die Darstellung von CCS-Programmen durch Petrinetze, Doctoral Diss., RWTH Aachen, 1988.

    Google Scholar 

  13. C.A.R. Hoare, Some properties of predicate transformers, J. ACM 25 (1978) 461–480.

    Article  MATH  MathSciNet  Google Scholar 

  14. C.A.R. Hoare, A calculus of total correctness for communicating processes, Sci. Comput. Progr. 1 (1981) 44–72.

    MathSciNet  Google Scholar 

  15. C.A.R. Hoare, Communicating Sequential Processes (Prentice-Hall, London, 1985).

    MATH  Google Scholar 

  16. B. Jonsson, Compositional Verification of Distributed Systems, Ph.D. Thesis, Dept. Comput. Sci., Uppsala Univ., 1987.

    Google Scholar 

  17. P.E. Lauer, P.R. Torrigiani, M.W. Shields, COSY - A system specification language based on paths and processes, Acta Inform. 12 (1979) 109–158.

    Article  MATH  Google Scholar 

  18. A. Mazurkiewicz, Concurrent program schemes and their interpretations, Tech. Report DAIMI PB-78, Aarhus Univ., 1977.

    Google Scholar 

  19. R. Milner, A Calculus of Communicating Systems, Lecture Notes in Comput. Sci. 92 (Springer-Verlag, 1980).

    Google Scholar 

  20. R. Milner, Communication and Concurrency (Prentice-Hall, London, 1989).

    MATH  Google Scholar 

  21. J. Misra, K.M. Chandy, Proofs of networks of processes, IEEE Trans. Software Eng. 7 (1981) 417–426.

    Article  MathSciNet  Google Scholar 

  22. E.-R. Olderog, Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship, Habilitationsschrift, Univ. Kiel, 1988/89.

    Google Scholar 

  23. E.-R. Olderog, Strong bisimilarity on nets: a new concept for comparing net semantics, in: J.W. de Bakker, W.P. de Roever, G. Rozenberg (Eds.), Linear Time, Branching Time and Partial Order in Logics and Models of Concurrency, Lecture Notes in Comput. Sci. 354 ( Springer-Verlag, 1989) 549–573.

    Google Scholar 

  24. E.-R. Olderog, Correctness of concurrent processes, invited paper, in: A. Kreczmar, G. Mirkowska (Eds.), Math. Found. of Comput. Sci. 1989, Lecture Notes in Comput. Sci. 379 (Springer-Verlag, 1989) 107–132.

    Google Scholar 

  25. E.-R. Olderog, C.A.R. Hoare, Specification-oriented semantics for communicating processes, Acta Inform. 23 (1986) 9–66.

    Article  MATH  MathSciNet  Google Scholar 

  26. S. Owicki, L. Lamport, Proving liveness properties of concurrent programs, ACM TOPLAS 4 (1982) 199–223.

    Article  Google Scholar 

  27. W. Reisig, Petri Nets, An Introduction, EATCS Monographs on Theoret. Comput. Sci. ( Springer-Verlag, 1985).

    Google Scholar 

  28. M. Rem, Trace theory and systolic computation, in: J.W. de Bakker, A.J. Nij-man, P.C. Treleaven (Eds.), Proc. PARLE Conf., Eindhoven, Vol. I, Lecture Notes in Comput. Sci. 258, ( Springer-Verlag, 1987) 14–33.

    Google Scholar 

  29. D.S. Scott, Outline of a mathematical theory of computation, Tech. Monograph PRG-2, Progr. Research Group, Oxford Univ., 1970.

    Google Scholar 

  30. J.E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory (MIT Press, Cambridge, Mass., 1977).

    Google Scholar 

  31. J.L.A. van de Snepscheut, Trace Theory and VLSI Design, Lecture Notes in Comput. Sci. 200 ( Springer-Verlag, 1985).

    Google Scholar 

  32. J. Widom, D. Gries, F.B. Schneider, Completeness and incompleteness of trace-baced network proof systems, in: Proc. 14th ACM Symp. on Principles of Progr. Languages, München, 1987, 27–38.

    Google Scholar 

  33. N. Wirth, Program development by stepwise refinement, Comm. ACM 14 (1971) 221–227.

    Article  MATH  Google Scholar 

  34. J. Zwiers, Compositionality, Concurrency and Partial Correctness, Lecture Notes in Comput. Sci. 321 ( Springer-Verlag, 1989).

    Google Scholar 

  35. J. Zwiers, W.P. de Roever, P. van Emde-Boas, Compositionality and concurrent networks, in: W. Brauer (Ed.), Proc. 12th Coll. Automata, Languages and Programming, Lecture Notes in Comput. Sci. 194 ( Springer-Verlag, 1985) 509–519.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FB Informatik, Universität Oldenburg, Postfach 2503, 2900, Oldenburg, Fed. Rep. Germany

    Ernst-Rüdiger Olderog

Authors
  1. Ernst-Rüdiger Olderog
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Technische Universität München, Postfach 202420, München 2, W-8000, Germany

    Manfred Broy

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Olderog, ER. (1992). Systematic Derivation of Communicating Programs. In: Broy, M. (eds) Programming and Mathematical Method. NATO ASI Series, vol 88. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-77572-7_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-77572-7_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-77574-1

  • Online ISBN: 978-3-642-77572-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation