Feature refinement
Files
360.3Kb
Citation
Export citationReeves, 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
2007Publisher
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.