An Approach to Combining B and Alloy
In this paper we propose to combine two software verification approaches, theorem proving and model checking. We focus on the B-method and a theorem proving tool associated with it, and the Alloy specification notation and its model checker “Alloy Constraint Analyser”. We consider how software development in B can be assisted using Alloy and how Alloy can be used for verifying refinement of abstract specifications. We demonstrate our approach with an example.
Unable to display preview. Download preview PDF.
- 1.J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
- 2.B-Core (UK) Limited, Oxon, UK. B-Toolkit, On-line manual., 1999. Available at http://www.b-core.com/ONLINEDOC/Contents.html.
- 3.S. Bensalem, C. Muñoz, S. Owre, H. Rueß, J. Rushby, V. Rusu, H. Saïdi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. In C. M. Holloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop, pages 187–196, Hampton, VA, June 2000. NASA Langley Research Center.Google Scholar
- 4.J. C. Bicarregui and B. M. Matthews. Proof and refutation in formal software development. In 3rd Irish Workshop on Formal Software Development, http://www.ewic.org.uk, July 1999. British Computer Society, Electornic Workshops in Computing.
- 5.Formal Systems (Europe) Ltd. Failures-Divergence Refinement-FDR2 user manual, October 1997. Available at http://www.formal.demon.co.uk.
- 6.M. Gordon. Introduction to the HOL system. In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors, Proceedigns of the International Workshop on the HOL Theorem Proving System and its Applications, pages 2–3, Los Alamitos, CA, USA, Aug. 1992. IEEE Computer Society Press.Google Scholar
- 8.D. Jackson. Alloy: A lightweight object modelling notation. MIT Lab for Computer Science, July 2000.Google Scholar
- 9.D. Jackson, I. Schechter, and I. Shlyakhter. Alcoa: the alloy constraint analyser. In Proc. International Conference on Software Engineering, Limerick, Ireland, June 2000.Google Scholar
- 10.K. MacMillan. The SMV Language. Cadence Berkeley Labs, 1999.Google Scholar
- 11.K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.Google Scholar
- 12.L. Mikhailov and M. Butler. Combining B and Alloy. In Proceedings of FMICS’2001, pages 29–45, Paris, July 2001. INRIA.Google Scholar
- 13.N. Shankar and J. M. Rushby. PVS Tutorial. Computer Science Laboratory, SRI International, Menlo Park, CA, Feb. 1993. Also appears in Tutorial Notes, Formal Methods Europe’ 93: Industrial-Strength Formal Methods, pages 357–406, Odense, Denmark, April 1993.Google Scholar
- 14.J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1987.Google Scholar
- 16.M. Woodman and B. Heal. Introduction to VDM. McGraw-Hill, 1993. ISBN 0-07-707434-3.Google Scholar