Loading...
Thumbnail Image
Item

Feature refinement

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
Type
Conference Contribution
Type of thesis
Series
Citation
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.
Date
2007
Publisher
IEEE Computer Society
Degree
Supervisors
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.