Abstract
Event-B is one of more popular notations for model-based, proof-driven specification. It offers a fairly high-level mathematical language based on FOL and ZF set theory and an economical yet expressive modelling notation. Model correctness is established by proving a number of conjectures constructed via a syntactic instantiation of schematic conditions. A significant part of provable conjectures requires proof hints from a user. For larger models this becomes extremely onerous as identical or similar proofs have to be repeated over and over, especially after model refactoring stages. In the paper we discuss an approach to making proofs more generic and thus less fragile and more reusable. The crux of the technique is offering an engineer an opportunity to complete a proof by positing and proving a generic lemma that may be reused in the same or even another project. To assess the technique potential we have developed a plug-in to the Rodin Platform and used it to prove a number of pre-existing Event-B models.
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
Notes
- 1.
There are, however, cases where the modeller’s insight is critical in providing a witness or case split. These, we believe, should be handled at the specification as discussed, for instance, in [10].
References
Event-B and the Rodin Platform. http://www.event-b.org/
Furst, A.: Event-B model of the Order/Supply Chain A2A Communication. http://deploy-eprints.ecs.soton.ac.uk/129/
Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
Abrial, J.-R.: Modelling in Event-B. Cambridge University Press, Cambridge (2010)
de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Butler, M., Maamria, I.: Practical theory extension in Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 67–81. Springer, Heidelberg (2013)
Clearsy. Atelier B.: User and Reference Manuals. http://www.atelierb.societe.com/index_uk.html
Marché, C., Paskevich, A., Bobot, F., Filliâtre, J.-C.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53–64, August 2011
Hallerstede, S.: On the purpose of Event-B proof obligations. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 125–138. Springer, Heidelberg (2008)
Hoang, T.S.: Proof hints for Event-B (2012). CoRR, abs/1211.1172
Iliasov, A., Bryans, J.: A proof-based method for modelling timed systems. In: Voronkov, A., Virbitskaite, I. (eds.) PSI 2014. LNCS, vol. 8974, pp. 161–176. Springer, Heidelberg (2015)
Industrial deployment of system engineering methods providing high dependability and productivity (DEPLOY), IST FP7 project. http://www.deploy-project.eu/
Burdy, L.: Automatic refinement. In: Proceedings of BUGM at FM 1999 (1999)
Conchon, S., Contejean, É., Kanig, J., Lescuyer, S.: CC(X): semantical combination of congruence closure with solvable theories. In: Post-proceedings of the 5th International Workshop on Satisfiability Modulo Theories (SMT 2007), vol. 198, no. 2 of Electronic Notes in Computer Science, pp. 51–69. Elsevier Science Publishers (2008)
Rigorous Open Development Environment for Complex Systems (RODIN), IST FP6 STREP project. http://rodin.cs.ncl.ac.uk/
Iliasov, A., Stankaitis, P., Adjepon-Yamoah, D., Romanovsky, A.: Rodin platform Why3 plug-in. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 275–281. Springer, Heidelberg (2016). doi:10.1007/978-3-319-33600-8_21
Said, M.Y., Butler, M., Snook, C.: Language and tool support for class and state machine refinement in UML-B. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 579–595. Springer, Heidelberg (2009)
Hoang, T.S.: Event-B model of the Buyer/Seller B2B Communication. http://deploy-eprints.ecs.soton.ac.uk/128/
The RODIN platform. http://rodin-b-sharp.sourceforge.net/
TPTP: Thousands of Problems for Theorem Provers. www.tptp.org/
Deharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in Rodin. Sci. Comput. Program. 94(Part 2), 130–143 (2014)
Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Freitas, L., Whiteside, I.: Proof patterns for formal methods. In: Proceedings of FM 2014: Formal Methods - 19th International Symposium, Singapore, 12–16 May 2014, pp. 279–295 (2014)
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009)
Acknowledgments
This work is supported by the RSSB/UK project SafeCap+: SafeCap for integrated optimum capacity, safety and energy strategies at multiple nodes, the EPSRC/UK project STRATA: Layers for Structuring Trustworthy Ambient Systems and the EPSRC IAA account project on Formal Data Analytics in Railway.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Iliasov, A., Stankaitis, P., Romanovsky, A. (2016). Proving Event-B Models with Reusable Generic Lemmas. In: Ogata, K., Lawford, M., Liu, S. (eds) Formal Methods and Software Engineering. ICFEM 2016. Lecture Notes in Computer Science(), vol 10009. Springer, Cham. https://doi.org/10.1007/978-3-319-47846-3_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-47846-3_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47845-6
Online ISBN: 978-3-319-47846-3
eBook Packages: Computer ScienceComputer Science (R0)