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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi and L. Lamport. The existence of refinement mappings. In Proc. 3rd IEEE Symp. on LICS, Edinburgh, 1988.
K. R. Apt and E.-R. Olderog. Proof rules dealing with fairness. Science of Computer Programming, 3:65–100, 1983.
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.
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.
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.
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.
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.
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.
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.
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.
R. J. R. Back and K. Sere. An implementation of action systems in occam. (in preparation), 1989.
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.
R. Bagrodia. An environment for the design and performance analysis of distributed systems. PhD thesis, The University of Texas at Austin, Austin, Texas, 1987.
K. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
P. Eklund. Synchronizing multiple processes in common handshakes. Reports on computer science and mathematics 39, Åbo Akademi, 1985.
N. Francez. Fairness. Springer-Verlag, 1986.
D. Harel. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 8(3):231–274, 1987.
C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, August 1978.
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
INMOS Ltd. occam Programming Manual. Prentice-Hall International, 1984.
B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Dept. of Computer Systems, Uppsala University, Uppsala, 1987. Available as report DoCS 87/09.
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.
R. Kurki-Suonio and T. Kankaanpää. On the design of reactive systems. BIT, 28(3):581–604, 1988.
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.
L. Lamport. Reasoning about nonatomic operations. In Proc. 10th ACM Conference on Principles of Programming Languages, pages 28–37, 1983.
L. Lamport. A simple approach to specifying concurrent systems. Communications of the ACM, 32(1):32–45, January 1989.
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.
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.
R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes of Computer Science. Springer Verlag, 1980.
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.
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.
K. Sere. Stepwise removal of virtual channels in distributed algorithms. In 2nd International Workshop on Distributed Algorithms, 1987.
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.
E. W. Stark. Proving entailment between conceptual state specifications. Theoretical Comput. Sci., 56:135–154, 1988.
Author information
Authors and Affiliations
Editor information
Rights 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