Model-checking CSP-Z: strategy, tool support and industrial application

Model-checking is now widely accepted as an efficient method for analysing computer system properties, such as deadlock-freedom. Its practical applicability is due to existing automatic tools which deal with tedious proofs. Another research area of increasing interest is formal language integration where the capabilities of each language are used to capture precisely some aspects of a system. In this paper we propose a general strategy for model-checking CSP-Z specifications using as tool support the FDR model-checker. The CSP-Z language is a semantical integration of CSP and Z, such that CSP handles the concurrent aspects of a system, and Z the data structures part. We also present a modular approach for model-checking complex CSP-Z specifications, specifically to verify deadlock-freedom. Finally, we present a CSP-Z specification for a subset of a real Brazilian artificial microssatellite, and apply the proposed strategy to prove that this specification is deadlock-free.