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

    Research output: Contribution to journalArticlepeer-review


    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.
    Original languageEnglish
    Pages (from-to)113-131
    Number of pages18
    JournalFormal Aspects of Computing
    Issue number1
    Publication statusPublished - Jan 2011


    • Event-B
    • Incremental development
    • Refinement
    • Retrenchment
    • Rodin toolset
    • Tower pattern
    • UseCase-wise development


    Dive into the research topics of 'Retrenchment for Event-B: UseCase-wise development and Rodin integration'. Together they form a unique fingerprint.

    Cite this