UseCase-wise development: Retrenchment for event-B

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    UseCase-wise Development, the introduction of functionality into an application in stages, with each stage being carried through to (ideally) implementation before the next is considered, is examined with a view to 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 Event-B. The details of an Event-B formulation of retrenchment, aligned to the practical details of the Rodin toolset, are described. The details of refinement/retrenchment interworking needed to handle UseCase-wise development are outlined, and a simple case study is given. © 2008 Springer-Verlag Berlin Heidelberg.
    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.
    PublisherSpringer Nature
    Number of pages13
    ISBN (Print)3540876022, 9783540876021
    Publication statusPublished - 2008
    Event11th International Symposium on Recent Advances in Intrusion Detection, RAID 2008 - London
    Duration: 1 Jul 2008 → …


    Conference11th International Symposium on Recent Advances in Intrusion Detection, RAID 2008
    Period1/07/08 → …


    • Event-B
    • Incremental Development
    • Refinement
    • Retrenchment
    • Tower Pattern
    • UseCase-wise development


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

    Cite this