Home

Welcome to the Circus2ZCSP wiki!

1. What's Circus2ZCSP?
2. Release notes
3. How to use Circus2ZCSP?
4. The context of Circus2ZCSP in my research?
5. How to build Circus2ZCSP?
6. Design

What's Circus2ZCSP?

Circus2ZCSP is a translator to link a Circus model to a CSP || Z model which is finally model-checked by ProB. Actually Z is translated into internal B by ProZ, a translator from Z to B in ProB. So eventually it is a CSP || B model. The theory behind is published in this paper: Model checking of state-rich formalism Circus by linking to CSP || B

The Context of Circus2ZCSP in my Research?

My research is about model checking of Circus by linking to CSP || B. It consists of several steps:

• Parse and typecheck the original Circus model, such as buffer_spec.tex. [Parser and typechecker from CZT, but have integrated in Circus2ZCSP]
• Translate parsed and typechecked Abstract Syntax Tree (AST+) from Circus to CSP || Z, output two files buffer_spec_csp.csp and buffer_spec_z.tex. [In Circus2ZCSP]
• Then use modified ProB to check this CSP || Z model. Z actually will be translated to internal B representation by ProZ in ProB. [In ProB]

The tools and case studies can be found here (Circus-Programs).