|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
| ASCII Text | x | ||
| Steve Reeves, David Streader, "Feature Refinement," Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), pp. 371-380, Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007. | |||
| BibTex | x | ||
| @article{ 10.1109/SEFM.2007.14, author = {Steve Reeves and David Streader}, title = {Feature Refinement}, journal ={Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)}, volume = {0}, year = {2007}, isbn = {0-7695-2884-8}, pages = {371-380}, doi = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2007.14}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) TI - Feature Refinement SN - 0-7695-2884-8 SP371 EP380 A1 - Steve Reeves, A1 - David Streader, PY - 2007 KW - null VL - 0 JA - Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) ER - | |||
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