Abstract
An experiment to incorporate retrenchment into the B-Toolkit is described. The syntax of a retrenchment construct is given, as is the proof obligation which gives retrenchment its semantics. The practical aspects of incorporating these into the existing B-Toolkit are then investigated. It transpires that the B-Toolkit’s internal architecture is heavily committed to monolithic refinement, because of B-Method philosophy, and this restricts what can be done without a complete rebuild of the toolkit. Experience with case studies is outlined.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B-Tool Reference Manual, Version 1.1. B-Core (UK) Ltd
Abrial, J.R.: The B Book. Cambridge University Press, Cambridge (1996)
Banach, R., Cross, R.: Safety requirements and fault trees using retrenchment. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) SAFECOMP 2004. LNCS, vol. 3219, pp. 210–223. Springer, Heidelberg (2004)
Banach, R., Jeske, C.: Output retrenchments, defaults, stronger compositions, feature engineering (2002) (Submitted)
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 Computer Science 11(5), 498–540 (1999)
Banach, R., Poppleton, M.: Engineering and theoretical underpinnings of retrenchment (2001) (Submitted)
Banach, R., Poppleton, M.: Retrenching partial requirements into system definitions: A simple feature interaction case study. Req. Eng. Journal 8, 266–288 (2002)
Behm, P., Desforges, P., Meynadier, J.-M.: Meteor: An industrial success in formal development. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, p. 26. Springer, Heidelberg (1998)
Desforges, P.: Using the b-method to design safety-critical software for railway systems. Recherche et Developpements - Fatis Marquant 97 (1998)
Essame, D.: Handling safety critical requirements in system engineering using the b formal method. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) SAFECOMP 2004. LNCS, vol. 3219, p. 115. Springer, Heidelberg (2004)
Fraser, S.: Mechanised Support for Retrenchment in the B-Toolkit, Master’s thesis, School of Computer Science, University of Manchester (2004)
Fraser, S.: Specifications, Proof Obligations and Proofs Supporting a Case Study of Retrenchment in the B-Toolkit (2004) Available online at, http://www.cs.man.ac.uk/~frasers/casestudy .
Haughton, H., Lano, K.: Specification in B: An Introduction Using the B-Toolkit. Imperial College Press, London (1996)
Poppleton, M., Banach, R.: Retrenchment: Extending the reach of refinement. In: Proc. ASE 1999, pp. 158–165. IEEE, Los Alamitos (1999)
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)
Schneider, S.: The B-Method: An Introduction. Palgrave (2001)
Sekerinski, E., Sere, K. (eds.): Program Development by Refinement. Springer, Heidelberg (1999)
Wordsworth, J.B.: Software Engineering with B. Addison-Wesley, Reading (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., Fraser, S. (2005). Retrenchment and the B-Toolkit. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds) ZB 2005: Formal Specification and Development in Z and B. ZB 2005. Lecture Notes in Computer Science, vol 3455. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11415787_13
Download citation
DOI: https://doi.org/10.1007/11415787_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25559-8
Online ISBN: 978-3-540-32007-4
eBook Packages: Computer ScienceComputer Science (R0)