Refinement and verification of concurrent systems specified in Object-Z and CSP
- 22 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The formal development of large or complex systems can often be facilitated by the use of more than one formal specification language. Such a combination of languages is particularly suited to the specification of concurrent or distributed systems, where both the modelling of processes and state is necessary. This paper presents an approach to refinement and verification of specifications written using a combination of Object-Z and CSP (communicating sequential processes). A common semantic basis for the two languages enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used for the Object-Z components of a specification, we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the CSP operators together with the logic for Object-Z.Keywords
This publication has 11 references indexed in Scilit:
- Unbounded nondeterminism in CSPPublished by Springer Nature ,2006
- Introduction to the ISO specification language LOTOSPublished by Elsevier ,2003
- Object-Z: A specification language advocated for the description of standardsComputer Standards & Interfaces, 1995
- A fully abstract semantics of classes for Object-ZFormal Aspects of Computing, 1995
- An Alternative Order for the Failures ModelJournal of Logic and Computation, 1992
- W: A Logic for ZPublished by Springer Nature ,1992
- The RAISE language, method and toolsFormal Aspects of Computing, 1989
- A state-based approach to communicating processesDistributed Computing, 1988
- An improved failures model for communicating processesPublished by Springer Nature ,1985
- A Theory of Communicating Sequential ProcessesJournal of the ACM, 1984