Retrenching the Purse: The Balance Enquiry Quandary, and Generalised and (1, 1) Forward Refinements

• Autorzy: Banach R. , Jeske C. , Poppleton M. , Stepney S.
• Języki publikacji: EN

Abstrakty

EN

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 briefly 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 recalled. One of the Mondex difficulties, the `Balance Enquiry Quandary' is treated in detail, and the way that retrenchment is able to account for the system behaviour is explained. The problem is reconsidered using generalised forward refinement, and the simplicity of the resolution of the quandary, both by retrenchment, and by generalised forward refinement, inspires the creation of a genuine (1,1) forward refinement for Mondex, something long thought impossible. The forward treatment exhibits a similar balance enquiry quandary to the backward refinement, as it must, given that both are refinements of an atomic action to a non-atomic protocol, and the forward quandary is dealt with as easily by retrenchment as is the backward case. The simplicity of the retrenchment treatment foreshadows a general purpose retrenchment Atomicity Pattern for dealing with atomic-versus-finegrained situations.

Słowa kluczowe

EN

retrenchment; refinement; verification; mondex purse; atomicity

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 1,2
• Strony: 29--69
• Opis fizyczny: bibliogr. 51 poz., wykr.

Twórcy

autor

Banach R.

autor

Jeske C.

autor

Poppleton M.

autor

Stepney S.

• School of Computer Science, University of Manchester, manchester M13 9PL. UK,

Bibliografia

• [1] Abrial, J.-R.: The B-Book: Assigning Programs to Meanings, Cambridge University Press, 1996.
• [2] Department of Trade and Industry: Information Technology Security Evaluation Criteria, 1991, Http://www.cesg.gov.uk/site/iacs/itsec/media/formal-docs/Itsec.pdf.
• [3] Banach, R., Jeske, C., Hall, A., Stepney, S.: Retrenchment and the Atomicity Pattern, Submitted.
• [4] Banach, R., Poppleton, M.: Retrenchment: An Engineering Variation on Refinement, 2nd International B Conference (D. Bert, Ed.), 1393, Springer, Montpellier, France, April 1998.
• [5] Banach, R., Poppleton, M.: Sharp Retrenchment, Modulated Refinement and Simulation, Formal Aspects of Computing, 11, 1999, 498-540.
• [6] Banach, R., Poppleton, M.: Engineering and Theoretical Underpinnings of Retrenchment, 2002, Submitted, http://www.cs.man.ac.uk/~banach/some.pubs/Retrench.Underpin.pdf.
• [7] Banach, R., Poppleton, M.: Retrenching Partial Requirements into System Definitions: A Simple Feature Interaction Case Study, Requirements Engineering Journal, 8(2), 2003, 266-288.
• [8] Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Retrenching the Purse: Finite Sequence Numbers and the Tower Pattern, Formal Methods 2005 (J. Fitzgerald, I. Hayes, T. A., Eds.), LNCS 3582, Springer, Newcastle, UK, 2005.
• [9] Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Retrenching the Purse: Finite Exception Logs, and Validating the Small, Software Engineering Workshop 30 (M. Hinchey, Ed.), IEEE, Layola College Graduate Center, Columbia, MD, 2006, To appear.
• [10] Banach, R., Poppleton, M., Jeske, C., Stepney, S.: Retrenching the Purse: Hashing Injective CLEAR Codes, and Security Properties, 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (B. Steffen, T. Margaria, Eds.), IEEE, Paphos, Cyprus, 2006, To appear.
• [11] Barthe, G., Courtieu, P., Dufay, P., de Sousa S., M.: Tool-assisted Specification and Verification of the JavaCard Platform, AMAST 2002 (H. Kirchner, C. Ringeissen, Eds.), 2422, Springer, 2002.
• [12] Behm, P., Desforges, P., J-M., M.: MéTéOR: An Industrial Success in Formal Development, in: Bowen et al. [26], 374-393.
• [13] Beierle, C., Börger, E.: Refinement of a typed WAM extension by polymorphic order-sorted types, Formal Aspects of Computing, 8(5), 1996, 539-564.
• [14] Beierle, C., Börger, E.: Specification and correctness proof of a WAM extension with abstract type constraints, Formal Aspects of Computing, 8(4), 1996, 428-462.
• [15] Bert, D., Bowen, J., King, S., Waldén, M., Eds.: Proc. ZB2003: Formal Specification and Development in Z and B, vol. 2651 of LNCS, Springer, Turku, Finland, June 2000.
• [16] Bicarregui, J., Ritchie, B.: Invariants, Frames and Postconditions: a Comparison of the VDM and B Notations, 670, Springer, 1993, ISBN 3-540-56662-7.
• [17] Börger, E.: A Logical Operational Semantics for Full Prolog. Part I: Selection Core and Control, CSL'89. 3rd Workshop on Computer Science Logic (E. Börger, H. Kleine Büning, M.M. Richter,W. Schönfeld, Eds.), 440, Springer-Verlag, 1990.
• [18] Börger, E.: A Logical Operational Semantics of Full Prolog. Part II: Built-in Predicates for Database Manipulation, in: Mathematical Foundations of Computer Science (B. Rovan, Ed.), vol. 452 of Lecture Notes in Computer Science, Springer-Verlag, 1990, 1-14.
• [19] Börger, E.: The ASM Refinement Method, Formal Aspects of Computing, 15, 2003, 237-275.
• [20] Börger, E., Del Castillo, G.: A formal method for provably correct composition of a real-life processor out of basic components (The APE100 Reverse Engineering Study), Proc. 1st IEEE Int. Conf. on Engineering of Complex Computer Systems (ICECCS'95) (B. Werner, Ed.), November 1995.
• [21] Börger, E., Durdanović, I.: Correctness of compiling Occam to Transputer code, Computer Journal, 39(1), 1996, 52-92.
• [22] Börger, E., Mazzanti, S.: A Practical Method for Rigorously Controllable Hardware Design, in: ZUM'97: The Z Formal Specification Notation (J. P. Bowen, M. B. Hinchey, D. Till, Eds.), vol. 1212 of Lecture Notes in Computer Science, Springer-Verlag, 1997, 151-187.
• [23] Börger, E., Rosenzweig, D.: The WAM - Definition and Compiler Correctness, in: Logic Programming: Formal Methods and Practical Applications (C. Beierle, L. Plümer, Eds.), North-Holland, 1994, 20-90.
• [24] Börger, E., Salamone, R.: CLAM Specification for Provably Correct Compilation of CLP(R) Programs, in: Specification and Validation Methods (E. Börger, Ed.), Oxford University Press, 1995, 97-130.
• [25] Börger, E., Stärk, R.: Abstract State Machines. A Method for High Level System Design and Analysis, Springer, 2003.
• [26] Bowen, J., Dunne, S., Galloway, A., King, S., Eds.: Proc. ZB2000: Formal Specification and Development in Z and B, vol. 1878 of LNCS, Springer, York, UK, August 2000.
• [27] Cooper, D., Stepney, S., Woodcock, J.: Derivation of Z Refinement Proof Rules, Technical Report YCS-2002-347, University of York, 2002.
• [28] Dawes, J.: The VDM-SL Reference Guide, UCL Press/ Pitman Publishing, London, 1991.
• [29] Derrick, J., Boiten, E.: Refinement in Z and Object-Z, FACIT, Springer, 2001.
• [30] Hall, A.: Using Formal Methods to Develop an ATC Information System, IEEE Software, 13, 1996, 66-76.
• [31] ISO 15408, v. 3.0 rev. 2: Common Criteria for Information Security Evaluation, 2005.
• [32] ISO/IEC 13568: Information Technology - Z Formal Specification Notation - Syntax, Type System and Semantics: International Standard, 2002, http://www.iso.org/iso/en/ittf/PubliclyAvailableStandards/c021573 ISO IEC 13568 2002(E).zip.
• [33] Jones, C.: Systematic Software Development using VDM, Second edition, Prentice-Hall, 1990.
• [34] Kleene, S.: Mathematical Logic, Wiley, 1967, also Dover 2002.
• [35] Lano, K., Haughton, H.: Specification in B: An Introduction Using the B-Toolkit, Imperial College Press, 1996.
• [36] RAISE Method Group: The RAISE Method Manual, Prentice Hall, 1995.
• [37] Schellhorn, G.: Verification of ASM Refinements Using Generalized Forward Simulation, JUCS, 7, 2001, 952-979.
• [38] Schellhorn, G.: ASM Refinement and Generalisations of Forward Simulation in Data Refinement: A Comparison, Theoretical Computer Science, 336, 2005, 403-435.
• [39] Schellhorn, G., Grandy, H., Haneberg, D., Reif,W.: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse, Technical Report 2006-02, Institut fur Informatik Universitat Augsburg, February 2006.
• [40] Schneider, S.: The B-Method, Palgrave Press, 2001.
• [41] Spivey, J.: The Z Notation: A Reference Manual, Second edition, Prentice-Hall, 1992.
• [42] Stärk, R., Schmidt, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation, Springer, 2000.
• [43] Stepney, S.: New Horizons in Formal Methods, The Computer Bulletin, 2001, 24-26.
• [44] Stepney, S., Cooper, D.: Formal Methods for Industrial Products, in: Bowen et al. [26], 374-393.
• [45] Stepney, S., Cooper, D., Woodcock, J.: More Powerful Z Data Refinement: Pushing the State of the Art. in Industrial Refinement, 11th International Conference of Z Users (J. Bowen, A. Fett, M. Hinchey, Eds.), 1493, Springer, Berlin, Germany, September 1998.
• [46] Stepney, S., Cooper, D., Woodcock, J.: An Electronic Purse: Specification, Refinement and Proof, Technical Report PRG-126, Oxford University Computing Laboratory, 2000.
• [47] Stepney, S., Polack, F., Toyn, I.: Patterns to Guide Practical Refactoring: examples targetting promotion in Z, in: Bert et al. [15], 20-39.
• [48] Stringer-Calvert, D. W. J., Stepney, S., Wand, I.: Using PVS to Prove a Z Refinement: a case study, FME '97: Formal Methods: Their Industrial Application and Strengthened Foundations, Graz, Austria, September 1997 (C. Jones, J. Fitzgerald, Eds.), 1313, Springer, 1997.
• [49] Teich, J., Kutter, P., Weper, R.: Description and Simulation of Microprocessor Instruction Sets Using ASMs, Abstract State Machines: Theory and Applications (Y. Gurevich, P. Kutter, M. Odersky, L. Thiele, Eds.), 1912, Springer-Verlag, 2000.
• [50] Van, H., George, C., Janowski, T., Moore, R.: Specification Case Studies in RAISE, FACIT, Springer, 2002.
• [51] Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof, Prentice-Hall, 1996.