This paper defines a new denotational semantics for the language of Communicating Sequential Processes (CSP). The semantics lies between the existing traces and failures models of CSP providing a treatment of non-determinism in terms of singleton failures. Although the semantics does not represent a congruence upon the full language it is adequate for sequential tests of non-deterministic processes. This semantics corresponds exactly to a commonly used notion of data refinement in Z and Object-Z: an abstract data type is refined when the corresponding process is refined in terms of singleton failures. The semantics is used to explore the relationship between data refinement and process refinement and to derive a rule for data refinement that is both sound and complete. BCS © 2006.

Original publication

DOI

10.1007/s00165-005-0081-x

Type

Journal article

Journal

Formal Aspects of Computing

Publication Date

01/06/2006

Volume

18

Pages

181 - 210