Model-checkign is now widely recognised as an efficient method for analysing computer system properties, such as deadlock-freedom. Its pracitcal applicability is due to existing automatic tools which deal with tedious proofs. Another increassigly research area is formal language integration where the capabilitie of each language are used to capture precisely some aspects of a system. In this paper we describe a formal strategy for deadlock analysis of specifications in CSP-Z. We also show how FDR(a model-checker originally developed for CSP) can be adapted for CSP-Z. Finally, we present a subset of a CSP-Z formal specification of a real Braxilian artificial microsatellite, and use FDR to check that the specification is deadlock-free.
展开▼
