csp2B: A Practical Approach to Combining CSP and B
- 1 November 2000
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 12 (3) , 182-198
- https://doi.org/10.1007/pl00003930
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.Keywords
This publication has 5 references indexed in Scilit:
- CSP-OZ: A Combination of Object-Z and CSPPublished by Springer Nature ,1997
- The B-BookPublished by Cambridge University Press (CUP) ,1996
- Stepwise refinement of communicating systemsScience of Computer Programming, 1996
- The temporal logic of actionsACM Transactions on Programming Languages and Systems, 1994
- Stepwise refinement of parallel algorithmsScience of Computer Programming, 1990