Abstract
The traces, failures, and divergences of CSP can be expressed as weakest precondition formulæ over action systems. We show how such systems may be refined up to failures-divergences, by giving two proof methods which are sound and jointly complete: forwards and backwards simulations. The technical advantage of our weakest precondition approach over the usual relational approach is in our simple handling of divergence; the practical advantage is in the fact that the refinement calculus for sequential programs may be used to calculate forwards simulations. Our methods may be adapted to state-based development methods such as VDM or Z.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
12 References
R-J.R. Back, “A Calculus of Refinements for Program Derivations”, Acta Informatica, 25, 593–624, 1988.
R-J.R. Back & R. Kurki-Suonio, “Decentralization of process nets with centralized control”, Proc 2nd Annual Symposium on Principles of Distributed Computing, Montreal, 1983.
E.W. Dijkstra, A Discipline of Programming, Prentice-Hall International, 1976.
He Jifeng, “Process refinement”, in The Theory and Practice of Refinement, J. McDermid (ed), Butterworths, 1989a.
—, “Specification and design of transaction processing system with various interfaces”, Procs REX Workshop on the Design of Distributed Systems, 1989b.
—, “A trace-state based approach to process specification and design”, Oxford University Computing Laboratory, Programming Research Group, 1989c.
—, C.A.R. Hoare, & J.W. Sanders, “Data refinement refined”, Lecture Notes in Computer Science, 213, 187–196, Springer-Verlag, 1986.
C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall International, 1985.
inmos, occam Programming Manual, Prentice-Hall International, 1984.
C.B. Jones, Systematic Software Development Using VDM, Prentice-Hall International, 1986.
M.B. Josephs, “A state-based approach to communicating processes”, Distributed Computing, 39–18, 1988.
R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, 92, Springer-Verlag, 1980.
Carroll Morgan, “The Specification Statement”, ACM TOPLAS, 10(3), 1988.
—, “Of wp and CSP”, Oxford University Computing Laboratory, Programming Research Group, 1989.
—, Programming from Specifications, Prentice-Hall International, in press, 1990.
— & P.H.B. Gardiner, “Data Refinement by Calculation”, Acta Informatica, To appear; reprinted in [Morgan, Robinson & Gardiner, 1988.
—, Ken Robinson, & Paul Gardiner, On the Refinement Calculus, Oxford University Computing Laboratory, Programming Research Group, Technical Monograph PRG-70, 1988.
J.M. Morris, “A Theoretical Basis for Stepwise Refinement and the Programming Calculus”, Science of Computer Programming, 9(3), 1987.
—, “Laws of Data Refinement”, Acta Informatica,, 26 287–308, 1989.
J.M. Spivey, The Z Notation: A Reference Manual, Prentice-Hall International, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Woodcock, J.C.P., Morgan, C. (1990). Refinement of state-based concurrent systems. In: Bjørner, D., Hoare, C.A.R., Langmaack, H. (eds) VDM '90 VDM and Z — Formal Methods in Software Development. VDM 1990. Lecture Notes in Computer Science, vol 428. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52513-0_18
Download citation
DOI: https://doi.org/10.1007/3-540-52513-0_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52513-4
Online ISBN: 978-3-540-47006-9
eBook Packages: Springer Book Archive