Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Refinement of Parallel and Reactive Programs

  • Conference paper

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

Abstract

We show how to apply the refinement calculus to stepwise refinement of parallel and reactive programs. We use action systems as our basic program model. Action systems are sequential programs which can be implemented in a parallel fashion. Hence refinement calculus methods, originally developed for sequential programs, carry over to the derivation of parallel programs. Refinement of reactive programs is handled by data refinement techniques originally developed for the sequential refinement calculus. We exemplify the approach by a derivation of a mutual exclusion algorithm.

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

Access this chapter

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. M. Abadi and L. Lamport. The existence of refinement mappings. InProc. $ni IEEE Symp. on LICS, Edinburgh, 1988.

    Google Scholar 

  2. R. J. R. Back.Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 ofMathematical Center Thacts. Mathematical Centre, Amsterdam, 1980.

    Google Scholar 

  3. R. J. R. Back. Changing data representation in the refinement calculus. In21st Hawaii International Conference on System Sciences. IEEE, January 1989.

    Google Scholar 

  4. R. J. R. Back. Refining atomicity in parallel algorithms. InPARLE 89 Parallel Architectures and Languages Europe, volume 366 of LectureNotes in Computer Science, Eindhoven, the Netherlands, June 1989. Springer Verlag, 1989.

    Google Scholar 

  5. R. J. R. Back. Refinement calculus II: Parallel and reactive programs. In J. W. deBakker, W. P. deRoever, and G. Rozenberg, editors,Stepwise Refinement of Distributed Systems, volume 430 ofLecture Notes in Computer Science, pages 6793. Springer Verlag, 1990.

    Google Scholar 

  6. R.J.R. Back. Refinement calculus, lattices, and higher order logic. This volume, p. 53.

    Google Scholar 

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

    Google Scholar 

  8. 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.

    Article MATH  Google Scholar 

  9. R. J. R. Back and R. Kurki-Suonio. Superposition and fairness in reactive system refinement. InJerusalem conference on Information Technology, Jerusalem, Israel, October 1990.

    Google Scholar 

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

    Google Scholar 

  11. R.J.R. Back and K. Sere. Deriving an occam implementation of action systems. In C. Morgan, J.C.P. Woodcock (eds.),Third BCS Refinement Workshop, pp. 9–30, Workshops in Computing, Springer-Verlag 1990.

    Google Scholar 

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

    Google Scholar 

  13. R.J.R. Back and J. von Wright. Refinement calculus I: Sequential nondeterministic programs. In J. W. deBakker, W.P. deRoever, and G. Rozenberg (eds.),Stepwise Refinement of Distributed Systems, Lecture Notes in Computer Science 430, pp. 42–66, Springer-Verlag, 1990.

    Google Scholar 

  14. 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 

  15. J. H. C.A.R. Hoare and J. Sanders. Prespecification in data refinement.Information Processing Letters, 25: 71–76, 1987.

    Article MathSciNet MATH  Google Scholar 

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

    Google Scholar 

  17. W. Chen and J. T. Udding. Towards a calculus of data refinement. In Mathematics of Program Construction, volume 375 ofLecture Notes in Computer Science, Groningen, The Netherlands, June 1989. Springer-Verlag.

    Google Scholar 

  18. P. Gardiner and C. Morgan. Data refinement of predicate transformers.Theoretical Comput. Sci., 87 (1): 143–162, 1991.

    Article MathSciNet MATH  Google Scholar 

  19. D. Cries and J. Prins. A new notion of encapsulation. InProc. SIGPLAN Symp. Language Issues in Programming Environments, June 1985.

    Google Scholar 

  20. C. A. R. Hoare. Proofs of correctness of data representation.Acta Informatica, 1 (4): 271–281, 1972.

    Article MATH  Google Scholar 

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

    Article MathSciNet MATH  Google Scholar 

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

    Google Scholar 

  23. C. Jones.Software Development: A Rigorous Approach. Prentice-Hall International, 1980.

    Google Scholar 

  24. 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 

  25. B. Jonsson. On decomposing and refining specifications of distributed systems. InREX Workshop for Refinement of Distributed Systems,volume 430 ofLecture Notes inComputer Science,Nijmegen, The Netherlands, 1989. Springer-Verlag.

    Google Scholar 

  26. 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 

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

    Google Scholar 

  28. L. Lamport. A Temporal Logic of Actions. Src report 57, Digital SRC, 1990.

    Google Scholar 

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

    Google Scholar 

  30. Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. InProc. 10thACM Symp. on Principles of Programming Languages, pages 141–154, 1983.

    Google Scholar 

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

    Google Scholar 

  32. C. Morgan and J. Woodcock. Of wp and CSP. InProceedings of VDM-91, 1991.

    Google Scholar 

  33. C. C. Morgan. Data refinement by miracles.Information Processing Letters, 26: 243–246, January 1988.

    Article MathSciNet  Google Scholar 

  34. J. M. Morris. Laws of data refinement.Acta Informatica, 26: 287–308, 1989.

    MathSciNet MATH  Google Scholar 

  35. S. Owicki and D. Cries. An axiomatic proof technique for parallel programs iActa Informatica, 6: 319–340, 1976.

    Article MATH  Google Scholar 

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

    Article MATH  Google Scholar 

  37. J. von Wright. Data refinement and the simulation method. Reports on computer science and mathematics 138, Abo Akademi, 1992.

    Google Scholar 

  38. J. von Wright. Data refinement with stuttering. Reports on computer science and mathematics 137, Abo Akademi, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    R. J. R. Back

Authors
  1. R. J. R. Back

    You can also search for this author inPubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Technische Universität München, Arcisstr. 21, D-80333, München, Germany

    Manfred Broy

Rights and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Back, R.J.R. (1993). Refinement of Parallel and Reactive Programs. In: Broy, M. (eds) Program Design Calculi. NATO ASI Series, vol 118. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-02880-3_3

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp