Specification Clones: An Empirical Study of the Structure of Event-B Specifications

  • Marie FarrellEmail author
  • Rosemary Monahan
  • James F. Power
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10469)


In this paper we present an empirical study of formal specifications written in the Event-B language. Our study is exploratory, since it is the first study of its kind, and we formulate metrics for Event-B specifications which quantify the diversity of such specifications in practice. We pay particular attention to refinement as this is one of the most notable features of Event-B. However, Event-B is less well-equipped with other standardised modularisation constructs, and we investigate the impact of this by detecting and analysing specification clones at different levels. We describe our algorithm used to identify clones at the machine, context and event level, and present results from an analysis of a large corpus of Event-B specifications. Our study contributes to furthering research into the area of metrics and modularisation in Event-B.



We would like to thank the anonymous reviewers for their feedback and Ruth O’Connor for her work on a preliminary version of our clone detector during her SPUR internship that was funded by Maynooth University.


  1. 1.
    Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)CrossRefGoogle Scholar
  2. 2.
    Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447–466 (2010)CrossRefGoogle Scholar
  3. 3.
    Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundamenta Informaticae 77(1–2), 1–28 (2007)MathSciNetzbMATHGoogle Scholar
  4. 4.
    Baxter, I.D., Yahin, A., Moura, L., Sant’Anna, M., Bier, L.: Clone detection using abstract syntax trees. In: International Conference on Software Maintenance, Maryland, USA, pp. 368–377 (1998)Google Scholar
  5. 5.
    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). doi: 10.1007/978-3-642-39698-4_5CrossRefGoogle Scholar
  6. 6.
    Farrell, M., Monahan, R., Power, J.F.: Providing a semantics and modularisation constructs for Event-B using institutions. In: International Workshop on Algebraic Development Techniques, Gregynog, Wales (2016)Google Scholar
  7. 7.
    Fürst, A.: Design patterns in Event-B and their tool support. Master’s thesis, Department of Computer Science, ETH Zürich, March 2009Google Scholar
  8. 8.
    Gondal, A., Poppleton, M., Snook, C.: Feature composition-towards product lines of Event-B models. In: International Workshop on Model-Driven Product Line Engineering, Twente, The Netherlands, pp. 18–25 (2009)Google Scholar
  9. 9.
    Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ilic, D., Latvala, T.: Supporting reuse in Event B development: modularisation approach. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 174–188. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-11811-1_14CrossRefGoogle Scholar
  10. 10.
    Kitchenham, B., Madeyski, L., Budgen, D., Keung, J., Brereton, P., Charters, S., Gibbs, S., Pohthong, A.: Robust statistical methods for empirical software engineering. Empir. Softw. Eng. 22(2), 579–630 (2017)CrossRefGoogle Scholar
  11. 11.
    Morgan, C., Robinson, K., Gardiner, P.: On the Refinement Calculus. Springer, London (1988)Google Scholar
  12. 12.
    Olszewska, M., Sere, K.: Specification metrics for Event-B developments. In: International Conference on Quality Engineering in Software Technology, Dresden, Germany (2010)Google Scholar
  13. 13.
    Pitu, M., Grijincu, D., Li, P., Saleem, A., Monahan, R., O’Donoghue, D.P.: Arís: analogical reasoning for reuse of implementation & specification. In: International Workshop on Artificial Intelligence for Formal Methods, Rennes, France, pp. 13–16 (2013)Google Scholar
  14. 14.
    Poppleton, M.: The composition of Event-B models. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 209–222. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-87603-8_17CrossRefzbMATHGoogle Scholar
  15. 15.
    Roy, C.K., Zibran, M.F., Koschke, R.: The vision of software clone management: past, present, and future. In: Software Maintenance, Reengineering and Reverse Engineering, Antwerp, Belgium, pp. 18–33 (2014)Google Scholar
  16. 16.
    Sanella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Software Development. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-17336-3CrossRefGoogle Scholar
  17. 17.
    Silva, R., Butler, M.: Supporting reuse of Event-B developments through generic instantiation. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 466–484. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-10373-5_24CrossRefGoogle Scholar
  18. 18.
    Silva, R., Pascal, C., Hoang, T.S., Butler, M.: Decomposition tool for event-B. Softw. Practice Exp. 41(2), 199–208 (2011)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Marie Farrell
    • 1
    Email author
  • Rosemary Monahan
    • 1
  • James F. Power
    • 1
  1. 1.Department of Computer ScienceMaynooth UniversityMaynoothIreland

Personalised recommendations