Towards Reuse with "Feature-Oriented Event-B"

Event-B [MAV:05] is a language for the formal specification and verification of reactive systems. The language and its RODIN toolkit represent a leading model-based technology for formal software construction. However, scalability is a major current concern, especially the dimension of reusability. We outline a proposed infrastructure for scalable development with reuse for Event-B. We focus specifically on our agenda for reuse in Software Product Lines, and explain how a form of feature modelling will be central to this programme.