Industrial deployment of system engineering methods providing high dependability and productivity


Specification Metrics for Event-B Developments

Olszewska, Marta and Sere, Kaisa (2010) Specification Metrics for Event-B Developments. In: CONQUEST 2010, 20-22 September 2010, Dresden, Germany.

PDF - Published Version


In this paper we define several metrics for Event-B specifications in order to as-sess the maintainability of a rigorous system in its early development stage. We perform measurements of physical features of the specification. Moreover, we derive metrics like difficulty of constructing a specification or effort needed for its creation. The specification is investigated in the perspective of its syntactical characteristics. We base our metrics on the Event-B language primitives, namely operators and operands that we regard meaningful for our measurement model. We also use statistics about proof obligations in our metrics, as we consider the proving activity as a vital element in the process of creating a specification. Presented metrics are applied to a number of Event-B specifications, both their dynamic and static parts. They are examined in order to empirically con-firm appropriateness for management purposes. Obtained results are analysed in a perspective of an abstract specification and its consecutive refinements.

Item Type:Conference or Workshop Item (Paper)
Subjects:Industrial Deployment > Space
Methodology > Other
Tool developments > Model construction
Tool developments > Rodin platform
Event-B > Event-B Theory
ID Code:249
Deposited By:Ms Marta Olszewska
Deposited On:26 Oct 2010 07:06
Last Modified:26 Oct 2010 07:08

Repository Staff Only: item control page

Deploy-Project - All right reserved