School of Computing

Incompleteness of relational simulations in the blocking paradigm

Eerke Boiten and John Derrick

Science of Computer Programming, 75:182-196, December 2010 [doi].

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.

Download publication 192 kbytes (PDF)

Bibtex Record

@article{3023,
author = {Eerke Boiten and John Derrick},
title = {Incompleteness of Relational Simulations in the Blocking Paradigm},
month = {December},
year = {2010},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {10.1016/j.scico.2010.07.003},
url = {http://www.cs.kent.ac.uk/pubs/2010/3023},
    volume = {75},
    issue = {12},
    publication_type = {article},
    submission_id = {8393_1279836528},
    ISSN = {0167-6423},
    journal = {Science of Computer Programming},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014