Incompleteness of Relational Simulations in the Blocking Paradigm

Boiten, Eerke and Derrick, John (2010) Incompleteness of Relational Simulations in the Blocking Paradigm. Science of Computer Programming, 75 (12). pp. 1262-1269. ISSN 0167-6423. (Full text available)

PDF (NOTICE: this is the author’s version of a work that was accepted for publication in Science of Computer Programming. Changes resulting from the publishing process may not be reflected in this document.) - Accepted Version
Download (197kB) Preview
[img]
Preview
Official URL
http://www.cs.kent.ac.uk/pubs/2010/3023

Abstract

Refinement is the notion of development between formal specifications. For specifications given in a relational formalism, downward and upward simulations are the standard method to verify that a refinement holds, their usefulness based upon their soundness and joint completeness. This is known to be true for total relational specifications and has been claimed to hold for partial relational specifications in both the non-blocking and blocking interpretations. In this paper we show that downward and upward simulations in the blocking interpretation, where domains are ''guards'', are not jointly complete. This contradicts earlier claims in the literature. We illustrate this with an example (based on one recently constructed by Reeves and Streader) and then construct a proof to show why joint completeness fails in general.

Item Type: Article
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group
Depositing User: Eerke Boiten
Date Deposited: 21 Sep 2012 09:49
Last Modified: 12 Dec 2013 11:49
Resource URI: http://kar.kent.ac.uk/id/eprint/30612 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year