Model checking of state-rich formalism Circus by linking to CSP ∥ B

Since state-rich formalism Circus is a combination of Z, CSP, refinement calculus and Dijkstra's guarded commands, its model checking is intrinsically more complicated and difficult than that of individual state-based languages or process algebras. Current solutions translate executable constructs of Circus programs to Java with JCSP, or translate them to CSP processes. Data aspects of Circus programs are expressed in the Java programming language or as CSP processes. Both of them have disadvantages. This work presents a new approach to model-checking Circus by linking it to CSP parallel to B; then we utilise ProB to model-check and animate the CSP parallel to B program. The most significant advantage of this approach is the direct mapping of the state part in Circus to Z and finally to B, which maintains the high-level abstraction of data specification. In addition, introduction of deadlock, invariant violation checking, LTL formula checking and animation is another key advantage. We present our approach, a link definition for a subset of Circus constructs, as well as a popular case study ( reactive buffer) to show the practical usability of our work. We conclude with a discussion of related work, advantages and potential limitations of our approach and future work.