Affordable Access

Capability and potential for formal feature-oriented reuse in Event-B

Publication Date
  • Qa75 Electronic Computers. Computer Science
  • Qa76 Computer Software


Capability & Potential for Formal Feature-oriented Reuse in Event-B Ali Gondal, Michael Poppleton, Michael Butler School of Electronics and Computer Science, University of Southampton, Southampton, SO17 1BJ, UK Abstract Context: Event-B is a leading state-based language for formal mod- elling and verification of systems supported by an extensible Rodin toolkit. Its existing composition techniques provide a starting point for the investiga- tion of capability for reuse via feature-based modelling. We contribute early methodology for formal development of software product lines (SPLs). An SPL is a set of related products built from a shared set of resources with a common base and having variabilities. Feature modelling has been widely used as a technique for building SPLs. Objective: Our objective is to explore existing capability and future po- tential for Event-B, in the formal modelling, verification and reuse of domain assets, ultimately targeting verifiable SPL development. We will also suggest further requirements for tools and techniques in Event-B/Rodin for formal product line modelling. Method: By modelling two-case studies in Event-B using different mod- elling styles, we explore current capability for feature modelling in Event- B. We show that Event-B decomposition techniques can be exploited for problem-space feature decomposition and solution-space architectural com- position. We have also developed a feature-modelling tool for Event-B to experiment with our example case-studies. Results: The case-study experiments show that the existing Event-B techniques can be used for feature-based modelling and revealed further re- quirements for feature modelling tool support. A guideline for feature-based modelling with Event-B/Rodin has been proposed based on the case-study experiments that could be used to achieve the benefits of reusing formal models. Conclusions: By providing a prototype tool and guidelines for feature May 24, 2012 modelling in Event-B, we can fo

There are no comments yet on this publication. Be the first to share your thoughts.