Farrell, Marie and Monahan, Rosemary and Power, James F. (2017) Specification Clones: An Empirical Study of the Structure of Event-B Specifications. In: SEFM 2017: Software Engineering and Formal Methods. Lecture Notes in Computer Science (LNCS) (10469). Springer, pp. 152-167. ISBN 9783319661964

Preview

Download (417kB) | Preview

Abstract

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.

Item Type:	Book Section
Additional Information:	Cite as: Farrell M., Monahan R., Power J.F. (2017) Specification Clones: An Empirical Study of the Structure of Event-B Specifications. In: Cimatti A., Sirjani M. (eds) Software Engineering and Formal Methods. SEFM 2017. Lecture Notes in Computer Science, vol 10469. Springer, Cham
Keywords:	Structure; Event-B Specifications; Event-B language;
Academic Unit:	Faculty of Science and Engineering > Computer Science
Item ID:	10222
Identification Number:	https://doi.org/10.1007/978-3-319-66197-1_10
Depositing User:	Dr. James Power
Date Deposited:	15 Nov 2018 18:19
Publisher:	Springer
Refereed:	Yes
Funders:	Irish Research Council (IRC)
URI:	https://link.springer.com
Use Licence:	This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

Repository Staff Only(login required)

Item control page

Downloads

Origin of downloads