Measurement Plug-In

Introduction

The measurement plugin to the RODIN platform will provide information both about the model itself and about the process of building the model. It has a double purpose:

• provide feedback to the user about the quality of the Event-B model he is building and about potential problems in it or in the way he is building it.
• automate the data collection process for the measurement and assessment WP. This data collected will be analyzed to identify global transfer (increase in model quality, size, complexity,...), tool shortcomings (usability, prover), modelling issues (to be addressed by training, language, tool evolution,...), etc.

This work is planned for project year 2. This chapter introduces the main requirements of the tool. A more detailed analysis is available in deliverables of the measurement WP:

• D7 for a state of the art about metrics for formal models
• D10 for technologies identified to implement the plug-in

Requirements

The plug-in will fulfill the following functional requirements

• evaluation of low-level model metrics, such as number of events, refinements, etc
• evaluation of relevant quality metrics such as complexity, maintainability, etc
• evaluation of tasks related metric such as time spend in modelling, proving or other activities (possibly based on other plugins) such as requirements, model-checking.
• The user will be given the ability to enable or disable the collection of task related metrics.

and the following non-functional requirements:

• usability: integration into RODIN, in the Event-B perspective as an additional view
• reactivity: metrics will be updated regularly (at an adequate pace, possibly incrementally) or at user request
• efficiency: metric evaluation will not significantly slow down the interactivity of the RODIN platform
• security: strict data management policy to enforce confidentiality of the models, especially the user must be able to see if the plug-in is enabled and no data can leave the tool without the user consent