Smith, G. and Derrick, J. (2001) Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Formal Methods in Systems Design, 18 (3). pp. 249-284. ISSN 0925-9856 .
|The full text of this publication is not available from this repository. (Contact us about this Publication)|
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.
|Subjects:||Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,|
|Divisions:||Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group|
|Depositing User:||Mark Wheadon|
|Date Deposited:||24 Nov 2008 17:59|
|Last Modified:||06 Jul 2009 10:54|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/13612 (The current URI for this page, for reference purposes)|
- Depositors only (login required):