Paper Info
Title
Refinement in Object-Z and CSP
Abstract
In this paper we explore the relationship between refinement in Object-Z and refinement in CSP. We prove with a simple counterexample that refinement within Object-Z, established using the standard simulation rules, does not imply failures-divergences refinement in CSP. This contradicts accepted results.Having established that data refinement in Object-Z and failures refinement in CSP are not equivalent we identify alternative refinement orderings that may be used to compare Object-Z classes and CSP processes. When reasoning about concurrent properties we need the strength of the failures-divergences refinement ordering and hence identify equivalent simulation rules for Object-Z. However, when reasoning about sequential properties it is sufficient to work within the simpler relational semantics of Object-Z. We discuss an alternative denotational semantics for CSP, the singleton failures semantic model, which has the same information content as the relational model of Object-Z.
Year
Venue
Keywords
2002
IFM
alternative denotational semantics,Object-Z class,failures refinement,simpler relational semantics,equivalent simulation rule,failures-divergences refinement,semantic model,alternative refinement ordering,data refinement,relational model
Field
DocType
ISBN
Programming language,Refinement calculus,Concurrency,Computer science,Denotational semantics,Theoretical computer science,Counterexample,Relational model,Object-Z,Formal verification,Semantic data model
Conference
3-540-43703-7
Citations 
PageRank 
References 
15
0.86
9
Authors
2
Name
Order
Citations
PageRank
Christie Bolton11329.27
Jim Davies267380.95