Skip to main content
SpringerLink
Log in
Book cover

Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems)

REX 1993: A Decade of Concurrency Reflections and Perspectives pp 622–684Cite as

Partial order based design of concurrent systems

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 803))

Abstract

A partial order based graph model for concurrency is introduced, using hierarchical structured graphs with relations denoting concurrency, causal ordering, and temporal ordering. Both compositionally structured processes as well as partial order based structures describing the semantics of processes can be expressed in this unified framework. Thus we obtain a powerful calculus that allows to algebraically transform processes or to prove properties of them.

Apart from algebraic properties we also study state based properties of the process language, by means of assertional techniques. We use the combination of the two to derive, in a number of transformation and refinement steps, a distributed minimum weight spanning tree algorithm, in the style of Gallagher, Humblet, and Spira.

Part of this work has been supported by Esprit/BRA Project 6021 (REACT).

The authors thank Mannes Poel for detailed comments on the manuscript and fruitful discussions.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K.R. Apt and E.-R. Olderog. Verification of sequential and concurrent programs. Springer-Verlag, 1991.

    Google Scholar 

  2. P.A. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987.

    Google Scholar 

  3. O. Boruvka. O jistém problému minimálním (in czech). Práca Moravské Přírodovědecké Společnosti, 3, 1926.

    Google Scholar 

  4. R.J.R. Back and K. Sere. Stepwise refinement of action systems. Structured Programming, 12:17–30, 1991.

    Google Scholar 

  5. C. Chou and E. Gafni. Understanding and verifying distributed algorithms using stratified decomposition. In Proc. 7th ACM Symposium on Principles of Distributed Computing. ACM, 1988.

    Google Scholar 

  6. K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.

    Google Scholar 

  7. W.P. de Roever. The quest for compositionality — a survey of assertion-based proof systems for concurrent programs, Part I: concurrency based on shared variables. In Proceedings of the IFIP Working Conference 1985: The role of abstract models in computer science, pages 181–207. North-Holland, 1985.

    Google Scholar 

  8. Elrad and N. Francez. Decomposition of distributed programs into communication closed layers. Science of Computer Programming, 2, 1982.

    Google Scholar 

  9. M. Fokkinga, M. Poel, and J. Zwiers. Modular completeness for communication closed layers. In Eike Best, editor, Proceedings CONCUR '93, Lecture Notes in Computer Science 715, pages 50–65. Springer-Verlag, 1993.

    Google Scholar 

  10. R.T. Gallager, P.A. Humblet, and P.M. Spira. A distributed algorithm for minimumweight spanning trees. ACM TOPLAS, 5(1):66–77, Jan 1983.

    Google Scholar 

  11. J. L. Gischer. Partial Orders and the Axiomatic Theory of Shuffle. PhD thesis, Stanford University, 1984.

    Google Scholar 

  12. R. Gerth and L. Shira. On proving communication closedness of distributed layers. In Proc. 6th Conference on Foundations of Software Technology and Theoretical Computer Science, 1986.

    Google Scholar 

  13. David Harel. Statecharts, a visual approach to complex systems. Technical Report CS86-02, Weizmann Institute of Science, March 1986.

    Google Scholar 

  14. J. Hooman and W.P. de Roever. The quest goes on: a survey of proof systems for partial correctness of CSP. In Current Trends in Concurrency, pages 343–395. LNCS 224, Springer-Verlag, 1986.

    Google Scholar 

  15. C.A.R. Hoare. Proofs of correctness of data representations. Acta Informatica, 1:271–281, 1972.

    Google Scholar 

  16. C.B. Jones. Systematic Software Development using VDM. Prentice-Hall, second edition, 1990.

    Google Scholar 

  17. W. Janssen, M. Poel, and J. Zwiers. Action systems and action refinement in the development of parallel systems. In Proc. of CONCUR '91, pages 298–316. Springer-Verlag, LNCS 527, 1991.

    Google Scholar 

  18. W. Janssen and J. Zwiers. From sequential layers to distributed processes, deriving a distributed minimum weight spanning tree algorithm, (extended abstract). In Proc. 11th ACM Symposium on Principles of Distributed Computing, pages 215–227. ACM, 1992.

    Google Scholar 

  19. W. Janssezn and J. Zwiers. Protocol design by layered decomposition, a compositional approach. In J.Vytopil, editor,Proc.Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 307–326. Springer-Verlag, LNCS 571, 1992.

    Google Scholar 

  20. W. Janssen and J. Zwiers. Specifying and proving communication closedness in protocols. Technical Report 93-23, University of Twente, 1993.

    Google Scholar 

  21. W. Janssen and J. Zwiers. Specifying and proving communication closedness in protocols. In A. Dantine, G. Leduc, and P. Wolper, editors, Proceedings 13th IFIP symp. on Protocol Specification, Testing and Verification, pages 323–339. Elsevier Science Publishers, 1993.

    Google Scholar 

  22. S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6(2), 1992.

    Google Scholar 

  23. N. Lynch, M. Merritt, W. Weihl, and A. Fekete. Atomic Transactions. Morgan Kaufman Publishers, 1994.

    Google Scholar 

  24. L.D. Loyens. A design method for parallel programs. PhD thesis, Eindhoven University of Technology, 1992.

    Google Scholar 

  25. A. Mazurkiewicz. Basic notions of trace theory. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proc. of the REX workshop on Linear Time, Branching Time and Partial order in Logics and Models for Concurrency, Noordwijkerhout 1988, Springer LNCS 354, pages 285–363, 1989.

    Google Scholar 

  26. R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

    Google Scholar 

  27. Carroll Morgan. Programming from Specifications. Prentice-Hall, 1990.

    Google Scholar 

  28. Wojciech Penczek. Axiomatizations of temporal logics on trace systems. In P. Enjalbert, A. Finkel, and K. Wagner, editors, LNCS 665, Proc. of STACS, pages 452–462. Springer-Verlag, 1993.

    Google Scholar 

  29. V. Pratt. Modelling concurrency with partial orders. International Journal of Parallel Programming, 1(15):33–71, 1986.

    Google Scholar 

  30. M. Poel and J. Zwiers. Layering techniques for development of parallel systems. In Proc. CAV, 1992.

    Google Scholar 

  31. F.A. Stomp and W.-P. de Roever. A correctness proof of a distributed minimum-weight spanning tree algorithm (extended abstract). In Proc. of the 7th ICDCS, 1987.

    Google Scholar 

  32. F.A. Stomp and W.P. de Roever. Designing distributed algorithms by means of formal sequentially phased reasoning. In J.-C. Bermond and M. Raynal, editors, Proc. of the 3rd International Workshop on Distributed Algorithms, Nice, LNCS 392, pages 242–253. Springer-Verlag, 1989.

    Google Scholar 

  33. K. Sere. Stepwise Derivation of Parallel Algorithms. PhD thesis, Åbo Akademi, 1990.

    Google Scholar 

  34. F.A. Stomp. Design and Verification of Distributed Network Algorithms: Foundations and Applications. PhD thesis, Eindhoven University, 1989.

    Google Scholar 

  35. A. S. Tanenbaum. Computer Networks. Prentice-Hall, second edition, 1988.

    Google Scholar 

  36. R.E. Tarjan. Data Structures and Network Algorithms. Society for Industrial and Apllied Mathematics, 1983.

    Google Scholar 

  37. J. Welch, L. Lamport, and N. Lynch. A lattice-structured proof technique applied to a minimum weight spanning tree algorithm. In Proc. of the 7th Annual Symp. on Principles of Distributed Computing. ACM, 1988.

    Google Scholar 

  38. J. Zwiers, W.-P. de Roever, and P. van Emde Boas. Compositionality and concurrent networks: Soundness and completeness of a proof system. In Proc. of ICALP '85, Springer LNCS 194, pages 509–519. Springer-Verlag, 1985.

    Google Scholar 

  39. J. Zwiers. Compositionality, Concurrency and Partial Correctness. Springer LNCS 321, 1989.

    Google Scholar 

  40. J. Zwiers. Layering and action refinement for timed systems. In Proc. of the REX Workshop on Real Time: Theory and Practice, Mook, the Netherlands, June 3–7 1991. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dep. of Computer Science, University of Twente, P.O. Box 217, 7500, AE Enschede, The Netherlands

    Job Zwiers & Wil Janssen

Authors
  1. Job Zwiers
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wil Janssen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker W. -P. de Roever G. Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zwiers, J., Janssen, W. (1994). Partial order based design of concurrent systems. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) A Decade of Concurrency Reflections and Perspectives. REX 1993. Lecture Notes in Computer Science, vol 803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58043-3_30

Download citation

  • DOI: https://doi.org/10.1007/3-540-58043-3_30

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58043-0

  • Online ISBN: 978-3-540-48423-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation