Feature refinement

Reeves, Steve; Streader, David

doi:10.1109/SEFM.2007.14

Files

Feature refinement.pdf

360.3Kb

Reeves, S. & Streader, D. (2007). Feature refinement. In Proceedings of Fifth IEEE International Conference on Software Engineering and Formal Methods(SEFM 2007), 2007(pp. 371-380). Washington, DC,USA: IEEE.

Permanent Research Commons link: https://hdl.handle.net/10289/1788

Abstract

Development by formal stepwise refinement offers a guarantee that an implementation satisfies a specification. But refinement is frequently defined in such a restrictive way as to disallow some useful development steps. Here we de- fine feature refinement to overcome some limitations of re- finement and show its usefulness by applying it to examples taken from the literature.

Using partial relations as a canonical state-based semantics and labelled transition systems as a canonical event-based semantics, we degine functions formally linking the state- and event-based operational semantics. We can then use this link to move notions of refinement between the event- and state-based worlds.

An advantage of this abstract approach is that it is not restricted to a specific syntax or even a specific interpretation of the operational semantics

Date

2007

Type

Conference Contribution

Publisher

IEEE Computer Society

Rights

This article has been published in the Proceedings of Fifth IEEE International Conference on Software Engineering and Formal Methods(SEFM 2007), 2007. ©2007 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

Collections

Computing and Mathematical Sciences Papers [1284]