Abstract
The action system formalism [3] is a state-based approach to distributed computing. In this paper, it is shown how the action system formalism may be used to describe systems that interact with their environment through synchronised value-passing. Definitions and rules are presented for refining and decomposing such action systems into distributed implementations in which internal communication is also based on synchronised value-passing. Specification and refinement is similar to the refinement calculus approach [1, 10, 12]. The theoretical basis for communication and distribution is Hoare's CSP [6]. Use of the refinement and decomposition rules is illustrated by the design of an unordered buffer.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R.J.R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications. Tract 131, Mathematisch Centrum, Amsterdam, 1980.
R.J.R. Back. Refinement of parallel and reactive programs. In Marktoberdorf International Summer School — Program Design Calculi, July 1992.
R.J.R. Back and R. Kurki-Suonio. Decentralisation of process nets with centralised control. In 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983.
M.J. Butler. A CSP Approach To Action Systems. D.Phil. Thesis, Programming Research Group, Oxford University, 1992.
E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
Jonsson. On decomposing and refining specifications of distributed systems. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume LNCS 430. Springer-Verlag, 1990.
N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In 6th ACM Symp. on Principles of Distributed Computing, pages 137–151, 1987.
C.C. Morgan. Of wp and CSP. In W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and J. Misra, editors, Beauty is our business: a birthday salute to Edsger W. Dijkstra. Springer-Verlag, 1990.
C.C. Morgan. Programming from Specifications. Prentice-Hall, 1990.
C.C. Morgan, K.A. Robinson, and P.H.B. Gardiner. On the Refinement Calculus. Technical Monograph PRG-70, Programming Research Group, Oxford University, October 1988.
J.M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Sci. Comp. Prog., 9(3):298–306, 1987.
J.C.P. Woodcock and C.C. Morgan. Refinement of state-based concurrent systems. In D. Bjørner, C.A.R. Hoare, and H. Langmaack, editors, VDM '90, volume LNCS 428. Springer-Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Butler, M.J. (1993). Refinement and decomposition of value-passing action systems. In: Best, E. (eds) CONCUR'93. CONCUR 1993. Lecture Notes in Computer Science, vol 715. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57208-2_16
Download citation
DOI: https://doi.org/10.1007/3-540-57208-2_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57208-4
Online ISBN: 978-3-540-47968-0
eBook Packages: Springer Book Archive