Specification, Refinement and Verification of Concurrent Systems-An Integration of Object-Z and CSP

摘要

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 allows classes specified in Object-Z to be Used directly within the CSP part of the specification.