Abstract
The Mondex Electronic Purse system [18] is an outstanding example of formal refinement techniques applied to a genuine industrial scale application, and notably, was the first verification to achieve ITSEC level E6 certification. A formal abstract model including security properties, and a formal concrete model of the system design were developed, and a formal refinement was hand-proved between them in Z. Despite this success, certain requirements issues were set beyond the scope of the formal development, or handled in an unnatural manner.
Retrenchment is reviewed in a form suitable for integration with Z refinement, and is used to address one such issue in detail: the finiteness of the transaction sequence number in the purse funds transfer protocol. A retrenchment is constructed from the lowest level model of the purse system to a model in which sequence numbers are finite, using a suitable elaboration of the Z promotion [21] technique. We overview the lifting of that retrenchment to the abstraction level of the higher models of the purse system. The concessions of the various retrenchments generated, formally capture the dissonance between the unbounded sequence number idealisation and the bounded reality. Reasoning about when the concession can become valid influences the actual choice of sequence number bound. The retrenchment-enhanced formal development is proposed as an example of a widely applicable methodological pattern for formal developments of this kind: the Tower Pattern.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Banach, R.: Maximally abstract retrenchments. In: Proc. IEEE ICFEM 2000, York, August 2000, pp. 133–142. IEEE Computer Society Press, Los Alamitos (2000)
Banach, R., Jeske, C., Poppleton, M.: Composition mechanisms for retrenchment (2004) (submitted), http://www.cs.man.ac.uk/~banach/some.pubs/Retrench.Composition.pdf.
Banach, R., Poppleton, M.: Retrenchment: An engineering variation on refinement. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 129–147. Springer, Heidelberg (1998)
Banach, R., Poppleton, M.: Sharp retrenchment, modulated refinement and simulation. Formal Aspects of Computing 11, 498–540 (1999)
Banach, R., Poppleton, M.: Retrenching partial requirements into system definitions: A simple feature interaction case study. Requirements Engineering Journal 8(2), 22 (2003)
Banach, R., Poppleton, M., Jeske, C.: Retrenchment and promotion in Z.(2004) (submitted for publication)
Bert, D., Bowen, J.P., King, S., Waldén, M. (eds.): ZB 2003. LNCS, vol. 2651. Springer, Heidelberg (2003)
Cooper, D., Stepney, S., Woodcock, J.: Derivation of Z refinement proof rules. Technical Report YCS-2002-347, University of York (2002)
de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)
Derrick, J., Boiten, E.: Refinement in Z and Object-Z. FACIT. Springer, Heidelberg (2001)
Grimmett, G., Stirzaker, D.: Probability and Random Processes, 3rd edn. O.U.P (2001)
Jeske, C.: Algebraic Integration of Retrenchment and Refinement. PhD thesis, University of Manchester (2005)
Karlin, S., Taylor, H.M.: A First Course in Stochastic Processes. Academic (1975)
Department of Trade and Industry. Information Technology Security Evaluation Criteria (1991), http://www.cesg.gov.uk/site/iacs/itsec/media/formal-docs/Itsec.pdf.
Poppleton, M., Banach, R.: Controlling control systems: An application of evolving retrenchment. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 42–61. Springer, Heidelberg (2002)
Resnick, S.L.: Adventures in Stochastic Processes. Birkhäuser, Basel (1992)
Stepney, S., Cooper, D., Woodcock, J.: More powerful Z data refinement: Pushing the state of the art in industrial refinement. In: P. Bowen, J., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 284–307. Springer, Heidelberg (1998)
Stepney, S., Cooper, D., Woodcock, J.: An electronic purse: Specification, refinement and proof. Technical Report PRG-126, Oxford University Computing Laboratory (2000)
Stepney, S., Polack, F., Toyn, I.: An outline pattern language for Z. In: Bert, et al. (eds.) [7], pp. 2–19.
Stepney, S., Polack, F., Toyn, I.: Patterns to guide practical refactoring. In: Bert, et al. (eds.) [7], pp. 20–39.
Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice-Hall, Englewood Cliffs (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Banach, R., Poppleton, M., Jeske, C., Stepney, S. (2005). Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_26
Download citation
DOI: https://doi.org/10.1007/11526841_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)