Skip to main content

Abstract Specification in Object-Z and CSP

Smith, Graeme and Derrick, John (2002) Abstract Specification in Object-Z and CSP. In: George, Chris and Miao, Huaikou, eds. Formal Methods and Software Engineering: 4th International Conference on Formal Engineering Methods. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 108-119. ISBN 978-3-540-00029-7. E-ISBN 978-3-540-36103-9. (doi:10.1007/3-540-36103-0_14) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)
Official URL
http://dx.doi.org/https://10.1007/3-540-36103-0_14

Abstract

A number of integrations of the state-based specification language Object-Z and the process algebra CSP have been proposed in recent years. In developing such integrations, a number of semantic decisions have to be made. In particular, what happens when an operation's precondition is not satisfied? Is the operation blocked, i.e., prevented from occurring, or can it occur with an undefined result? Also, are outputs from operations angelic, satisfying the environment's constraints on them, or are the demonic and not influenced by the environment at all? In this paper we discuss the differences between the models, and show that by adopting a blocking model of preconditions together with an angelic model of outputs one can specify systems at higher levels of abstraction.

Item Type: Book section
DOI/Identification number: 10.1007/3-540-36103-0_14
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 17:59 UTC
Last Modified: 30 Aug 2019 10:31 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/13698 (The current URI for this page, for reference purposes)
  • Depositors only (login required):