Relational Concurrent Refinement with Internal Operations and Outputs

This Web presentation shows a formalisation of the most important notions of the paper [BDS07]. The presentation is divided into four layers (called projects in KIV) of specifications and theorems:

Project DataRef specifies standard data refinement, and shows that forward and backward simulation imply refinement. This project also defines data types with internal and external operations (by partitioning the index set of a standard data type). The main specification defining such a data type is called weak-DT, since it was already used in [Sch05] to formalize weak refinement as defined in [DB01].
Project processDTRef specifies process data types with operations being triples consisting of the effective operation, a blocking range and a divergence range (defined in divblkOP and divblkDT ). Their proof obligations for forward and backward simulation are shown in forward and backward to be instances of standard data refinement via an embedding that uses a bottom element for blocking and an omega element for divergence. For comparison, an earlier version of process data types where divergence does not dominate blocking that was verified too is still available.
Project CSPRef defines failures and divergences for data types with internal and external operations. We prove that these definitions satisfy the axioms of CSP semantics . Proof obligations for forward and backward simulations are defined and shown here and here to be instances of those for process data types.
Project CSPRef-DataRef defines CSP-like data types, i.e. data types with internal and external operations, where finalisation is defined as refusals. We prove that refusals-divergence refinement for such data types is equivalent to defining refinement as data refinement using the embedding of the data types into process data types (as in the project above). The main proof is divided into two implications shown in FD-implies-DATA-refine and in DATA-implies-FD-refine . The most important theorems for one data type (Lemmas 1-3 in the paper) are shown in CSP-DT-ext

Bibliography

[DB01]	Refinement in Z and in Object-Z : Foundations and Advanced Applications, J. Derrick and E. Boiten, FACIT, Springer, 2001
[Sch05]	ASM Refinement and Generalizations of Forward Simulation in Data Refinement: A Comparison, G. Schellhorn, Journal of Theoretical Computer Science, vol. 336, no. 2-3, Elsevier, 403 - 435, 2005
[DBS07]	Relational Concurrent Refinement, Part II: Internal Operations and Outputs, J. Derrick, E. Boiten, G. Schellhorn , (under consideration for Formal Aspects of Computing)

[Imprint] [Data Privacy Statement] [E-Mail]