A Basis for Feature-Oriented Modelling in Event-B

Abstract

Feature-oriented modelling is a well-known approach for Software Product Line (SPL) development. It is a widely used method when developing groups of related software. With an SPL approach, the development of a software product is quicker, less expensive and of higher quality than a one-off development since much effort is re-used. However, this approach is not common in formal methods development, which is generally high cost and time consuming, yet crucial in the development of critical systems. With the increase of more complex critical systems, it becomes more important to apply formal methods to the development cycle, and we propose a method that allows the application of SPL development techniques to formal methods. This results in faster and cheaper development of formal systems. Our method combines Event-B [1] and feature models [2]. A feature in a feature model represents a requirement of the product family and is formally described in Event-B using special feature modelling patterns. A feature repre- sented in Event-B is referred to as component. We develop composition rules, which allow components to be composed. Special composition proof obligations allow the verification of the composition. The feature model is formed by features which may be associated with Event- B components. A subset of features from the feature model can be selected to form a feature model instance, thereby selecting several of these Event-B com- ponents. These components are composed pair-wise, and composition POs can be discharged to prove properties and to ensure consistency of the composition. The final Event-B machine represents the formal specification which is associated with the feature model instance and is obtained by composing these components. The motivation of our work is to allow product line development for critical systems. We use traditional product line methods, i.e. feature modelling, and link it with the formal method Event-B. Future work is focussed on amending feature diagrams to reflect Event-B components more precisely. Refinement patterns will also be addressed.