Skip to main content
SpringerLink
Log in

Refinement calculus, part II: Parallel and reactive programs

  • Technical Contributions
  • Conference paper
  • First Online:
Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness (REX 1989)

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

Abstract

It is shown how to apply the refinement calculus to stepwise refinement of both parallel programs and reactive programs. The approach is based on using the action systems model to describe parallel and reactive systems. Action systems are sequential programs which can be implemented in a parallel fashion. Hence the refinement calculus for sequential programs carries over to the parallel programs expressed in this framework. Refinement of reactive programs can be expressed and proved in the refinement calculus by using the methods of data refinement from the sequential refinement calculus.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi and L. Lamport. The existence of refinement mappings. In Proc. 3rd IEEE Symp. on LICS, Edinburgh, 1988.

    Google Scholar 

  2. K. R. Apt and E.-R. Olderog. Proof rules dealing with fairness. Science of Computer Programming, 3:65–100, 1983.

    Google Scholar 

  3. R. J. R. Back. Refining atomicity in parallel algorithms. In PARLE Conference on Parallel Architectures and Languages Europe, volume 366 of Lecture Notes in Computer Science, Eindhoven, the Netherlands, June 1989. Springer Verlag. Also available as Åbo Akademi reports on computer science and mathematics no. 57, 1988.

    Google Scholar 

  4. R. J. R. Back, E. Hartikainen, and R. Kurki-Suonio. Multi-process handshaking on broadcasting networks. Reports on computer science and mathematics 42, Åbo Akademi, 1985.

    Google Scholar 

  5. R. J. R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. In 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pages 131–142. ACM, 1983.

    Google Scholar 

  6. R. J. R. Back and R. Kurki-Suonio. Co-operation in distributed systems using symmetric multiprocess handshaking. Reports on computer science and mathematics 34, Åbo Akademi, 1984.

    Google Scholar 

  7. R. J. R. Back and R. Kurki-Suonio. Distributed co-operation with action systems. ACM Transactions on Programming Languages and Systems, 10:513–554, October 1988. Previous version in Åbo Akademi reports on computer science and mathematics no. 34, 1984.

    Article  Google Scholar 

  8. R. J. R. Back and R. Kurki-Suonio. Serializability in distributed systems with handshaking. In International Colloquium on Automata, Languages and Programming, volume 317 of Lecture Notes in Computer Science, 1988. Previous version in CMU-CS-85-109, Carnegie-Mellon University 1985.

    Google Scholar 

  9. R. J. R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. Distributed Computing, 3(2):73–87, 1989. Appeared previously in 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing 1983.

    Article  Google Scholar 

  10. R. J. R. Back and K. Sere. An exercise in deriving parallel algorithms: Gaussian elimination. Reports on computer science and mathematics 65, Åbo Akademi, 1988.

    Google Scholar 

  11. R. J. R. Back and K. Sere. An implementation of action systems in occam. (in preparation), 1989.

    Google Scholar 

  12. R. J. R. Back and K. Sere. Refinement of action systems. In Mathematics of Program Construction, volume 375 of Lecture Notes in Computer Science, Groningen, The Netherlands, June 1989. Springer-Verlag.

    Google Scholar 

  13. R. Bagrodia. An environment for the design and performance analysis of distributed systems. PhD thesis, The University of Texas at Austin, Austin, Texas, 1987.

    Google Scholar 

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

    Google Scholar 

  15. P. Eklund. Synchronizing multiple processes in common handshakes. Reports on computer science and mathematics 39, Åbo Akademi, 1985.

    Google Scholar 

  16. N. Francez. Fairness. Springer-Verlag, 1986.

    Google Scholar 

  17. D. Harel. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 8(3):231–274, 1987.

    Article  Google Scholar 

  18. C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, August 1978.

    Article  Google Scholar 

  19. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

    Google Scholar 

  20. INMOS Ltd. occam Programming Manual. Prentice-Hall International, 1984.

    Google Scholar 

  21. B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Dept. of Computer Systems, Uppsala University, Uppsala, 1987. Available as report DoCS 87/09.

    Google Scholar 

  22. R Kurki-Suonio and H.-M. Järvinen. Action system approach to the specification and design of distributed systems. In Proc. 5th International Workshop on Software Specification and Design, volume 14(3) of ACM Software Engineering Notes, pages 34–40, 1989.

    Google Scholar 

  23. R. Kurki-Suonio and T. Kankaanpää. On the design of reactive systems. BIT, 28(3):581–604, 1988.

    Google Scholar 

  24. S. S. Lam and A. U. Shankar. A relational notation for state transition systems. Technical Report TR-88-21, Dept. of Computer Sciences, University of Texas at Austin, 1988.

    Google Scholar 

  25. L. Lamport. Reasoning about nonatomic operations. In Proc. 10th ACM Conference on Principles of Programming Languages, pages 28–37, 1983.

    Google Scholar 

  26. L. Lamport. A simple approach to specifying concurrent systems. Communications of the ACM, 32(1):32–45, January 1989.

    Google Scholar 

  27. N. A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th ACM Symp. on Principles of Distributed Computing, pages 137–151, 1987.

    Google Scholar 

  28. Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In Proc. 10th ACM Symp. on Principles of Programming Languages, pages 141–154, 1983.

    Google Scholar 

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

    Google Scholar 

  30. J. Misra. Specifications of concurrently accessed data. In J. van de Snepscheut, editor, Mathematics of Program Construction, volume 375 of Lecture Notes in Computer Science, Groningen, The Netherlands, June 1989. Springer-Verlag.

    Google Scholar 

  31. A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In de Bakker, de Roever, and Rozenberg, editors, Current Trends in Concurrency, volume 224 of Lecture Notes in Computer Science, pages 510–584. Springer Verlag, 1986.

    Google Scholar 

  32. K. Sere. Stepwise removal of virtual channels in distributed algorithms. In 2nd International Workshop on Distributed Algorithms, 1987.

    Google Scholar 

  33. E. W. Stark. Foundations of a Theory of Specification for Distributed Systems. PhD thesis, Massachussetts Inst. of Technology, 1984. Available as Report No. MIT/LCS/TR-342.

    Google Scholar 

  34. E. W. Stark. Proving entailment between conceptual state specifications. Theoretical Comput. Sci., 56:135–154, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department ofComputer Science, Åbo Akademi University, Lemminkäinengatan 14, SF-20520, Åbo, Finland

    R. J. R. Back

Authors
  1. R. J. R. Back
    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

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Back, R.J.R. (1990). Refinement calculus, part II: Parallel and reactive programs. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness. REX 1989. Lecture Notes in Computer Science, vol 430. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52559-9_61

Download citation

  • DOI: https://doi.org/10.1007/3-540-52559-9_61

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52559-2

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation