Skip to main content
SpringerLink
Log in

Compositional Transformational Design for Concurrent Programs

  • Conference paper
  • First Online:
Compositionality: The Significant Difference (COMPOS 1997)

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

Included in the following conference series:

Abstract

Partial order based techniques are incorporated in a interleaving semantics, based on coding partial order information in linear time temporal logic. An example of development is given.

The authors thank mannes poel for collaboration and fruitful discussions

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. P. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987.

    Google Scholar 

  2. R. Back and K. Sere. Superposition refinement of parallel algorithms. InK.R. Parker and G.A. Rose, editors, Formal Description Techniques IV. IFIP Transaction C-2, North Holland, 1992.

    Google Scholar 

  3. C. Chou and E. Gafni.Understanding and verifying distributed algorithmsusing stratified decomposition. In Proceeding 7th ACM Symposium on Principles of Distributed Computing, 1988.

    Google Scholar 

  4. R. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison Wesley, 1988.

    Google Scholar 

  5. T. Elrad and N. Francez. Decomposition of distributed programs into communication closed layers. Science of Computer Programming, 2:155–173, 1982.

    Article  MATH  Google Scholar 

  6. M. Fokkinga, M. Poel, and J. Zwiers. Modular completeness for communication closed layers. In Eike Best, editor, Proceedings CONCUR’ 93, LNCS715, pages 50–65. Springer-Verlag, 1993.

    Google Scholar 

  7. R. Gallager, P. Humblet, and P. Spira. A distributed algorithm forminimum-weight spanning trees. ACM TOPLAS 5(1):66–77Jan1983.

    Google Scholar 

  8. R. Gerth and L. Shira. On proving communication closedness of distributedlayers. In Proceedings 6th Conference on Foundations of Software Technology and Theoretical Computer Science, 1986.

    Google Scholar 

  9. W. Janssen, M. Poel, Q. Xu, and J. Zwiers. Layering of real-time distributed processes. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors Proceedings Formal Techniques in Real Time and Fault Tolerant Systems LNCS 863, pages 393–417. Springer-Verlag, 1994.

    Google Scholar 

  10. W. Janssen, M. Poel, and J. Zwiers. Action systems and action refinementin the development of parallel systems. In Proceedings of CONCUR’91, LNCS 527, pages 298–316. Springer-Verlag, 1991.

    Google Scholar 

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

    Google Scholar 

  12. W. Janssen and J. Zwiers. Protocol design by layered decomposition, a com-positional approach. In J. Vytopil, editor, Proceedings Formal Techniques inReal-Time and Fault-Tolerant Systems, LNCS 571, pages 307–326. Springer-Verlag, 1992.

    Google Scholar 

  13. S. Katz. A superimposition control construct for distributed systems. ACM Transactions on Programming Languages and Systems, 15(2), 1993.

    Google Scholar 

  14. S. Katz and D. Peled. Interleaving set temporal logic. In Proceedings of the 6th ACM Symposium on Principles of Distributed Computing, Vancouver,pages 178–190, 1987.

    Google Scholar 

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

    Google Scholar 

  16. L. Lamport. Specifying concurrent program modules. ACM TOPLAS5(2)1983.

    Google Scholar 

  17. L. Lamport. What good is temporal logic. In Proc. IFIP 9th World Congress, pages 657–668, 1983.

    Google Scholar 

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

    Chapter  Google Scholar 

  19. Z. Manna and A. Pnueli. Adequate proof principles for invariance and live-ness properties. Science of Computer Programming, 4, 1984.

    Google Scholar 

  20. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems-Specification. Springer-Verlag, 1992.

    Google Scholar 

  21. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems-Safety.Springer-Verlag, 1995.

    Google Scholar 

  22. A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symp. on Foundations of Comp. Sci., pages 46–57, 1977.

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  24. A. Rensink and H. Wehrheim. Weak sequential composition in process algebras. In Proceedings CONCUR’ 94, LNCS 836, pages 226–241. Springer-Verlag, 1994.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  27. F. Stomp and W.-P. de Roever. A principle for sequential reasoning about distributed systems. Formal Aspects of Computing, 6(6):716–737, 1994.

    MATH  Google Scholar 

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

    Google Scholar 

  29. F. Stomp. A derivation of a broadcasting protocol using sequentially phased reasoning. In Stepwise refinement of distributed systems, LNCS 430, pages696–730. Springer-Verlag, 1990.

    Google Scholar 

  30. J. Zwiers and W. Janssen. Partial order based design of concurrent systems.In J. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX School/Symposium “A Decade of Concurrenyrd, Noordwijkerhout 1993, LNCS 803, pages 622–684. Springer-Verlag, 1994.

    Google Scholar 

  31. J. Zwiers. Layering and action refinement for timed systems. In de Bakker, Huizing, de Roever, and Rozenberg, editors Real-Time: Theory in Practice, LNCS 600, pages 687–723. Springer-Verlag, 1991.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Job Zwiers

Authors
  1. Job Zwiers
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Informatics and Applied Mathematics, Christian Albrechts University at Kiel, Preußerstr. 1-9, D-24105, Kiel, Germany

    Willem-Paul de Roever  & Hans Langmaack  & 

  2. Department of Applied Mathematics and Computer Science, Weizmann Institute of Science, P.O. Box 26, Rehovot, 76100, Israel

    Amir Pnueli

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zwiers, J. (1998). Compositional Transformational Design for Concurrent Programs. In: de Roever, WP., Langmaack, H., Pnueli, A. (eds) Compositionality: The Significant Difference. COMPOS 1997. Lecture Notes in Computer Science, vol 1536. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49213-5_24

Download citation

  • DOI: https://doi.org/10.1007/3-540-49213-5_24

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65493-3

  • Online ISBN: 978-3-540-49213-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation