Some of the success stories of model based refinement are recalled, as well as some of the annoyances that arise when refinement is deployed in the engineering of large systems. The way that retrenchment attempts to alleviate such inconveniences is reviewed. The Mondex Electronic Purse formal development provides a highly credible testbed for examining how real world refinement difficulties can be treated via retrenchment. The contributions of retrenchment to integrating the real implementation with the formal development are surveyed, and the extraction of commonly occurring 'retrenchment patterns' is suggested.
More on the
Full paper : PDF 62K
@inproceedings(SS-WSCS04,
author = "Richard Banach and Michael Poppleton and Czeslaw Jeske and Susan Stepney",
title = "Retrenchment and the Mondex Electronic Purse (extended abstract)",
crossref = "ASM05"
)
@proceedings(ASM05,
title = "Proc. 12th International Workshop on Abstract State Machines (ASM'05),
Paris, France, March 2005",
booktitle = "Proc. 12th International Workshop on Abstract State Machines (ASM'05),
Paris, France, March 2005",
editor = "D. Beauquier and E. Boerger and A. Slissenko",
year = 2005
)