Towards a model-checker for circus

Abstract

Among several approaches aiming at the correctness of systems, model-checking is one technique to formally assess system models regarding their desired/undesired behavioural properties. We aim at model-checking the Open image in new window notation that combines Z, CSP, and Morgan’s refinement calculus, based on the Unifying Theories of Programming. In this paper, we experiment with approaches for capturing Open image in new window processes in CSP, and for each approach, we evaluate the impact of our decisions on the state-space explored as well as the time spent for such a checking using FDR. We also experimented with the consequences of model-checking CSP models that capture both state invariants and preconditions of Open image in new window models.