{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T14:55:08Z","timestamp":1729608908734,"version":"3.28.0"},"reference-count":41,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007,9]]},"DOI":"10.1109\/sefm.2007.34","type":"proceedings-article","created":{"date-parts":[[2007,10,15]],"date-time":"2007-10-15T15:06:17Z","timestamp":1192460777000},"page":"37-46","source":"Crossref","is-referenced-by-count":2,"title":["Retrenchment and the Atomicity Pattern"],"prefix":"10.1109","author":[{"given":"Richard","family":"Banach","sequence":"first","affiliation":[]},{"given":"Czeslaw","family":"Jeske","sequence":"additional","affiliation":[]},{"given":"Anthony","family":"Hall","sequence":"additional","affiliation":[]},{"given":"Susan","family":"Stepney","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","article-title":"An electronic purse: Specification, refinement and proof","author":"stepney","year":"2000","journal-title":"Technical Report PRG-126"},{"journal-title":"Operating System Concepts","year":"2005","author":"silberschatz","key":"ref38"},{"journal-title":"Distributed Algorithms and Protocols","year":"1988","author":"raynal","key":"ref33"},{"key":"ref32","first-page":"814","author":"poppleton","year":"0","journal-title":"Structuring retrenchments in B by decomposition In Araki"},{"key":"ref31","article-title":"Retrenchment: Extending refinement for continuous and control systems","author":"poppleton","year":"2000","journal-title":"Proc IWFM'00"},{"journal-title":"Atomic Transactions","year":"1994","author":"lynch","key":"ref30"},{"key":"ref37","first-page":"16","article-title":"The Mondex challenge: Machine checked proofs for an electronic purse","volume":"4085","author":"schellhorn","year":"2006","journal-title":"Proc FM'2006"},{"key":"ref36","article-title":"A systematic verification approach for mondex electronic purses using ASMs","author":"schellhorn","year":"2007","journal-title":"Proc Dagstuhl 2007"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.013"},{"key":"ref34","first-page":"952","article-title":"Verification of ASM refinements using generalized forward simulation","volume":"7","author":"schellhorn","year":"2001","journal-title":"JUCS"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s00766-002-0157-6"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.340"},{"key":"ref11","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1007\/11526841_26","article-title":"Retrenching the purse: Finite sequence numbers and the tower pattern","volume":"3582","author":"banach","year":"0","journal-title":"FM 2005"},{"journal-title":"Principles of Concurrent Programming","year":"1982","author":"ben-ari","key":"ref12"},{"journal-title":"Concurrency Control and Recovery in Database Systems","year":"1987","author":"bernstein","key":"ref13"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0012-7"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7"},{"journal-title":"Database Systems A Practical Approach to Design Implementation and Management","year":"2004","author":"connolly","key":"ref16"},{"key":"ref17","article-title":"Derivation of Z refinement proof rules","author":"cooper","year":"2002","journal-title":"Technical Report YCS-2002–347"},{"journal-title":"Distributed Systems Concepts and Design","year":"2005","author":"coulouris","key":"ref18"},{"journal-title":"Department of Trade and Industry Information Technology Security Evaluation Criteria","year":"1991","key":"ref19"},{"journal-title":"Oracle database 10g - the complete reference","year":"2004","author":"loney","key":"ref28"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/800221.806716"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/169701.169682"},{"key":"ref3","volume":"2805","author":"araki","year":"2003","journal-title":"Proceedings of the International Symposium of Formal Methods Europe"},{"journal-title":"Composition mechanisms for retrenchment","year":"2004","author":"banach","key":"ref6"},{"journal-title":"Distributed Algorithms","year":"1996","author":"lynch","key":"ref29"},{"volume":"458","journal-title":"Proceedings of CONCUR 1990","year":"1990","key":"ref5"},{"key":"ref8","first-page":"129","article-title":"Retrenchment: An engineering variation on refinement","volume":"1393","author":"banach","year":"1998","journal-title":"2nd International Conference"},{"key":"ref7","first-page":"29","article-title":"Retrenching the purse: The balance enquiry quandary, and generalised and (1,1) forward refinements","volume":"77","author":"banach","year":"2007","journal-title":"Fund Inf"},{"key":"ref2","first-page":"222","article-title":"Refinement and reachability in Event-B","volume":"3455","author":"abrial","year":"0","journal-title":"Proc ZB-2005"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/ICFEM.2000.873814"},{"key":"ref1","first-page":"51","article-title":"Event based sequential program development: Application to constructing a pointer program","author":"abrial","year":"0","journal-title":"ARAKIS"},{"journal-title":"Fundamentals of Database Systems","year":"2003","author":"elmasri","key":"ref20"},{"journal-title":"Database Systems The Complete Book","year":"2003","author":"garcia-molina","key":"ref22"},{"key":"ref21","first-page":"230","article-title":"Superimposition for interactive processes","author":"francez","year":"0","journal-title":"Baeten and Klop"},{"journal-title":"Operating Systems Concurrent and Distributed Software Desien","year":"2003","author":"harris","key":"ref24"},{"journal-title":"Official Guide to DB2 Version 8","year":"2003","author":"zikopoulos","key":"ref41"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/52.506463"},{"journal-title":"Algebraic Integration of Retrenchment and Refinement","year":"2005","author":"jeske","key":"ref26"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-6217-7"}],"event":{"name":"Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007)","start":{"date-parts":[[2007,9,10]]},"location":"London, UK","end":{"date-parts":[[2007,9,14]]}},"container-title":["Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4343908\/4343909\/04343922.pdf?arnumber=4343922","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,17]],"date-time":"2017-06-17T23:54:54Z","timestamp":1497743694000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/4343922\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,9]]},"references-count":41,"URL":"https:\/\/doi.org\/10.1109\/sefm.2007.34","relation":{},"subject":[],"published":{"date-parts":[[2007,9]]}}}