Retrenchment for Event-B: UseCase-wise development and Rodin integration

Abstract

UseCase-wise Development, an 'Agile Method' which introduces functionality into an application stage by stage, with each stage being carried through (ideally) to implementation before the next is considered, is examinedwith a viewto its being treated via an Event-B methodology. The need to modify top level behaviour in a non-skip way precludes its naive treatment via Event-B refinement, and paves the way for the use of retrenchment in an Event-B context.AnEvent-B formulation of retrenchment aligned to the practicalities of theRodin toolset is described. The details of refinement/retrenchment interworking needed to handle UseCase-wise development are outlined, and three small case studies are discussed. The details of the integration of the retrenchment proposal into Rodin are outlined. BCS © 2009.