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. We present a method to integrate feature-oriented development with the formal specification language Event-B. Our approach allows the user to map a feature from the feature model to an Event-B component, which contains a formal specification of that feature. We also present some patterns, which assist the user in the modelling of EventB components. We describe a composition process which consists of the user selecting an instance in the feature model and then constructing this i...

• Type: Conference
• Year: 2010
• Where: ASM
• Authors: Jennifer Sorge, Michael Poppleton, Michael Butler
• Keywords: ASM 2010, Feature Model, Formal Specification, Microbiology, Software Product