The issues surrounding the question of atomicity, both in the past and nowadays, are briefly reviewed, and a picture of an ACID (atomic, consistent, isolated, durable) transaction as a refinement problem is presented. An example of a simple air traffic control system is introduced, and the discrepancies that can arise when read-only operations examine the state at atomic and finegrained levels are handled by retrenchment. Non-ACID timing aspects of the ATC example are also handled by retrenchment, and the treatment is generalised as the retrenchment Atomicity Pattern. The utility of the pattern is confirmed against a different case study, the Mondex Electronic Purse.
More on the
full paper : PDF 129K
@inproceedings(SS-SEFM07, author = "Richard Banach and Czeslaw Jeske and Anthony Hall and Susan Stepney", title = "Retrenchment and the Atomicity Pattern", crossref = "SEFM07" ) @proceedings(SEFM07, title = "5th IEEE International Conference on Software Engineering and Formal Methods: SEFM 07, London, UK, September 2007", booktitle = "5th IEEE International Conference on Software Engineering and Formal Methods: SEFM 07, London, UK, September 2007", publisher = "IEEE Press", year = 2007 )