Combining CSP and B for specification and property verification

Abstract

PROB is a model checking tool for the B Method. In this paper we present an extension of PROB that supports checking of specifications written in a combination of CSP and B. We explain how the notations are combined semantically and give an overview of the implementation of the combination. We illustrate the benefit that appropriate use of CSP, in conjunction with our tool, gives to B developments both for specification and for verification purposes. © Springer-Verlag Berlin Heidelberg 2005.