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 applica bility is due to existing automatic tools which deal with tedious proofs. A nother 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 specif ications, specifically to verify deadlock-freedom. Finally, we present a CS P-Z specification for a subset of a real Brazilian artificial microssatelli te, and apply the proposed strategy to prove that this specification is dea dlock-free. (C) 2001 Elsevier Science B.V. Ail rights reserved.