Abstract
This paper describes the tool csp2B which provides a means of combining CSP-like descriptions with standard B specifications. The notation of CSP provides a convenient way of describing the order in which the operations of a B machine may occur. The function of the tool is to convert CSP-like specifications into standard machine-readable B specifications which means that they may be animated and appropriate proof obligations may be generated. Use of csp2B means that abstract specifications and refinements may be specified purely using CSP or using a combination of CSP and B. The translation is justified in terms of an operational semantics.
Chapter PDF
Similar content being viewed by others
References
J.-R. Abrial. The B-Book. Cambridge University Press, 1996.
J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In D. Bert, editor, Second International B Conference, April 1998.
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.
M.J. Butler. An approach to the design of distributed systems with B AMN. In J.P. Bowen, M.G. Hinchey, and D. Till, editors, 10th International Conference of Z Users (ZUM’97), volume LNCS 1212, pages 223–241. Springer-Verlag, April 1997.
M.J. Butler. csp2B User Manual. Available from http://www.ecs.soton.ac.uk/~mjb/csp2B, 1999.
M.J. Butler and M. Waldén. Distributed system development in B. In H. Habrias, editor, First B Conference, November 1996.
P. Hartel, M. Butler, A. Currie, P. Henderson, M. Leuschel, A. Martin, A. Smith, U. Ultes-Nitsche, and B. Walters. Questions and answers about ten formal methods. In Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems, Trento, Italy, Jul 1999. http://www.dsse.ecs.soton.ac.uk/techreports/99-1.html.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
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.
A.W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1998.
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, pages 340–351. Springer-Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Butler, M. (1999). csp2B: A Practical Approach to Combining CSP and B. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1708. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48119-2_28
Download citation
DOI: https://doi.org/10.1007/3-540-48119-2_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66587-8
Online ISBN: 978-3-540-48119-5
eBook Packages: Springer Book Archive