Model-checking circus with FDR using circus2csp

Abstract

The current lack of tool support for model-checking Circus, a formalism which combines Z, CSP, refinement calculus and Dijkstra's guarded commands, is one of the constraints for its use at industrial scale. Nowadays, it is possible to translate Circus to other formalisms and to verify them profiting from existing model-checkers, such as FDR and ProB, which have no direct support for Circus. However, such approaches are usually performed manually, which requires time and also may introduce errors. We used Haskell to implement an automatic tool which preserves the semantics while translating Circus to CSP, which includes an automatic Circus refinement calculator as part of the transformation before the translation into CSP. It is based on the existing set of translation rules but has several improvements, compared to its original strategy. We extended the language coverage, and provide a more efficient structure for handling more complex type systems, and better support for specifications with larger sets of state variables. We introduce a set of translation rules for using Z schemas as Circus actions, not previously supported in the translation into CSP. In our research, we also explored ways of verifying the correctness of our implementation. We proved manually some interesting properties for the translation, which are related to the improvements developed in this work. We also investigated the use of Isabelle/UTP as a theorem prover in order to help us to increase confidence in our approach. However, our tool was tested using several Circus case-studies present in the literature. Among our findings, we observed that, compared to previous work, the state-space explored with our improved translation strategy was reduced dramatically by over eighty per cent and the time consumed for checks in FDR was reduced from minutes to milliseconds, compared to the initially adopted strategy.