School of Computing

Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP

G. Smith and J. Derrick

Formal Methods in Systems Design, 18:182-196, May 2001.

Abstract

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to be used directly within the CSP part of the specification.

In addition to specification, we also discuss refinement and verification in this model. The common semantic basis 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.



Bibtex Record

@article{1202,
author = {G. Smith and J. Derrick},
title = {Specification, refinement and verification of concurrent systems - an   integration of {Object-Z} and {CSP}},
month = {May},
year = {2001},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2001/1202},
    publication_type = {article},
    submission_id = {22725_989923839},
    journal = {Formal Methods in Systems Design},
    volume = {18},
    publisher = {Kluwer Academic Publishers},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014