© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Relational concurrent refinement II: Internal operations and outputs
E.A. Boiten, J. Derrick, and G. Schellhorn
Formal Aspects of Computing, 21(1-2):182-196, February 2009 [doi].Abstract
Two styles of description arise naturally in formal specification: state-based and behavioural. In state-based notations, a system is characterised by a collection of variables, and their values determine which actions may occur throughout a system history. Behavioural specifications describe the chronologies of actions -- interactions between a system and its environment. The exact nature of such interactions is captured in a variety of semantic models with corresponding notions of refinement; refinement in state based systems is based on the semantics of sequential programs and is modelled relationally. Acknowledging that these viewpoints are complementary, substantial research has gone into combining the paradigms.
The purpose of this paper is to do three things. First, we survey recent
results linking the relational model of refinement to the process algebraic
models.
Specifically, we detail how variations in the relational framework lead to
relational data refinement being in correspondence with traces-divergences,
singleton failures and failures-divergences refinement in a process semantics.
Second, we generalise these results by
providing a general flexible scheme for incorporating the two main
"erroneous" concurrent behaviours: deadlock and divergence, into relational
refinement. This is shown to subsume previous characterisations. In doing this
we derive relational refinement
rules for specifications containing both internal operations and outputs that
corresponds to failures-divergences refinement.
Third, the theory has been formally
specified and verified using the interactive theorem prover KIV.
Download publication
639 kbytes
(PostScript)
Bibtex Record
@article{2633, author = {E.A. Boiten and J. Derrick and G. Schellhorn}, title = {Relational Concurrent Refinement {II}: Internal Operations and Outputs}, month = {February}, year = {2009}, pages = {182-196}, keywords = {determinacy analysis, Craig interpolants}, note = {}, doi = {10.1007/s00165-007-0066-z}, url = {http://www.cs.kent.ac.uk/pubs/2009/2633}, publication_type = {article}, submission_id = {8932_1196088604}, ISSN = {0934-5043}, journal = {Formal Aspects of Computing}, volume = {21}, number = {1-2}, }