|
Published Articles >> Table of Contents >> Abstract
Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06)
pp. 60-69
Filtering Retrenchments into Refinements
Richard Banach, University of Manchester, UK
John Derrick, University of Sheffield, UK
Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2006.17
Send link to a friend
| Abstract |
|
Retrenchment is a weakening of model based refinement
that enables many development steps not expressible by
refinement to be formally described nevertheless. The
greater flexibility of retrenchment comes at the price of
much feebler guarantees as compared with refinement,
and so the interplay between retrenchment and refinement
can hope to offer the best of both worlds. The paper
explores the strategy of filtering the information in a
retrenchment to yield a refinement under a suitable notion
of observation. A general construction is given that enables
a retrenchment, with its intrinsic notion of observability,
to be filtered to produce a refinement with its intrinsic
notion of observability. A simple running example illustrates
the theory.
|
Additional Information
|
Citation:
Richard Banach, John Derrick,
"Filtering Retrenchments into Refinements,"
sefm,
pp. 60-69,
Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06),
2006
|
|