Retrenchment and the Mondex Electronic Purse

Richard Banach; Michael Poppleton; Czeslaw Jeske; Susan Stepney

Retrenchment and the Mondex Electronic Purse

Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney

Computer Science

Research output: Contribution to conference › Paper › peer-review

Abstract

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.

Original language	Undefined/Unknown
Pages	41-48
Publication status	Published - 2005

Access to Document

http://www.univ-paris12.fr/lacl/dima/asm05/ret.asm.mondex.short.ps

Cite this

@conference{feb1f598caa245af89576b1d82b22c2e,

title = "Retrenchment and the Mondex Electronic Purse",

abstract = "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.",

author = "Richard Banach and Michael Poppleton and Czeslaw Jeske and Susan Stepney",

year = "2005",

language = "Undefined/Unknown",

pages = "41--48",

}

TY - CONF

T1 - Retrenchment and the Mondex Electronic Purse

AU - Banach, Richard

AU - Poppleton, Michael

AU - Jeske, Czeslaw

AU - Stepney, Susan

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

M3 - Paper

SP - 41

EP - 48

ER -