%0 Journal Article %1 smith_01_specification %A Smith, Graeme %A Derrick, John %C Hingham, MA, USA %D 2001 %I Kluwer Academic Publishers %J Form. Methods Syst. Des. %K refinement verification object-z concurrency specification csp 2001 %N 3 %P 249--284 %R 10.1023/A:1011269103179 %T Specification, Refinement and Verification of Concurrent Systems---An Integration of Object-Z and CSP %U http://dx.doi.org/10.1023/A:1011269103179 %V 18 %X 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.

@article{smith_01_specification, 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.}, added-at = {2009-02-12T11:04:54.000+0100}, address = {Hingham, MA, USA}, author = {Smith, Graeme and Derrick, John}, biburl = {https://www.bibsonomy.org/bibtex/2dc45f8b1ba820d1e0298ab3e8945fe16/leonardo}, citeulike-article-id = {3578005}, doi = {10.1023/A:1011269103179}, interhash = {24c2c0a3d6d81ab4118355fa55afc346}, intrahash = {dc45f8b1ba820d1e0298ab3e8945fe16}, issn = {0925-9856}, journal = {Form. Methods Syst. Des.}, keywords = {refinement verification object-z concurrency specification csp 2001}, number = 3, pages = {249--284}, posted-at = {2009-02-02 19:57:36}, priority = {3}, publisher = {Kluwer Academic Publishers}, timestamp = {2009-02-12T11:04:54.000+0100}, title = {Specification, Refinement and Verification of Concurrent Systems---An Integration of Object-Z and CSP}, url = {http://dx.doi.org/10.1023/A:1011269103179}, volume = 18, year = 2001 }