Abstract
Refinement is a key concept in the B-Method. While refinement is at the heart of the B Method, so far no automatic refinement checker has been developed for it. In this paper we present a refinement checking algorithm and implementation for B. It is based on using an operational semantics of B, obtained in practice by the ProB animator. The refinement checker has been integrated into ProB toolset and we present various case studies and empirical results in the paper, showing the algorithm to be surprisingly effective. The algorithm checks that a refinement preserves the trace properties of a specification. We also compare our tool against the refinement checker FDR for CSP and discuss an extension for singleton failure refinement.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
Abrial, J.-R.: Case study of a complete reactive system in Event-B: A mechanical press controller. In: Tutorial at ZB 2005(2005), Available at http://www.zb2005.org/
Abrial, J.-R., Cansell, D.: Click’n prove: Interactive proofs within set theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 1–24. Springer, Heidelberg (2003)
Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, p. 83. Springer, Heidelberg (1998)
Basu, S., Mukund, M., Ramakrishnan, C.R., Ramakrishnan, I.V., Verma, R.M.: Local and symbolic bisimulation using tabled constraint logic programming. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol. 2237, pp. 166–180. Springer, Heidelberg (2001)
Bolton, C., Davies, J.: A comparison of refinement orderings and their associated simulation rules. Electr. Notes Theor. Comput. Sci. 70(3), 440–453 (2002)
Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221–236. Springer, Heidelberg (2005)
Butler, M.J.: An approach to the design of distributed systems with B AMN. In: Till, D., Bowen, P.J., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 223–241. Springer, Heidelberg (1997)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Dunne, S., Conroy, S.: Process refinement in B. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 45–64. Springer, Heidelberg (2005)
Farwer, B., Leuschel, M.: Model checking object Petri nets in Prolog. In: Proceedings PPDP 2004, pp. 20–31. ACM Press, New York (2004)
Formal Systems (Europe) Ltd. Failures-Divergence Refinement — FDR2 User Manual
Gardiner, P.H.B., Morgan, C.: A single complete rule for data refinement. Formal Asp. Comput. 5(4), 367–382 (1993)
He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Leuschel, M., Massart, T.: Infinite state model checking by abstract interpretation and program specialisation. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 63–82. Springer, Heidelberg (2000)
Leuschel, M., Turner, E.: Visualizing larger states spaces in ProB. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 6–23. Springer, Heidelberg (2005)
B-Core. B-toolkit manuals (1999)
Robinson, N.J.: Checking z data refinements using an animation tool. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 62–81. Springer, Heidelberg (2002)
Roscoe, A.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)
Sagonas, K., Swift, T., Warren, D.S.: XSB as an efficient deductive database engine. In: Proceedings SIGMOD 1994, Minneapolis, pp. 442–453. ACM, New York (1994)
Schneider, S., Treharne, H.: Communicating B machines. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 416–435. Springer, Heidelberg (2002)
Steria. Atelier B, user and reference manuals (1997)
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
Leuschel, M., Butler, M. (2005). Automatic Refinement Checking for B. In: Lau, KK., Banach, R. (eds) Formal Methods and Software Engineering. ICFEM 2005. Lecture Notes in Computer Science, vol 3785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11576280_24
Download citation
DOI: https://doi.org/10.1007/11576280_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29797-0
Online ISBN: 978-3-540-32250-4
eBook Packages: Computer ScienceComputer Science (R0)