UseCase-wise development: Retrenchment for event-B

Richard Banach

doi:10.1007/978-3-540-87603-8_14

UseCase-wise development: Retrenchment for event-B

Research output: Chapter in Book/Conference proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Publisher	Springer Nature
Pages	167-180
Number of pages	13
Volume	5238
ISBN (Print)	3540876022, 9783540876021
DOIs	https://doi.org/10.1007/978-3-540-87603-8_14
Publication status	Published - 2008
Event	11th International Symposium on Recent Advances in Intrusion Detection, RAID 2008 - London Duration: 1 Jul 2008 → …

Conference

Conference	11th International Symposium on Recent Advances in Intrusion Detection, RAID 2008
City	London
Period	1/07/08 → …

Keywords

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

Access to Document

10.1007/978-3-540-87603-8_14

Cite this

@inproceedings{ceb80f8f06de4bc9a668127c0af552f9,

title = "UseCase-wise development: Retrenchment for event-B",

abstract = "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. {\textcopyright} 2008 Springer-Verlag Berlin Heidelberg.",

keywords = "Event-B, Incremental Development, Refinement, Retrenchment, Tower Pattern, UseCase-wise development",

author = "Richard Banach",

note = "British Comp Soc, Facs Nokia praxis Banach, Richard 16 BERLIN BIJ68; 11th International Symposium on Recent Advances in Intrusion Detection, RAID 2008 ; Conference date: 01-07-2008",

year = "2008",

doi = "10.1007/978-3-540-87603-8_14",

language = "English",

isbn = "3540876022",

volume = "5238",

pages = "167--180",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

publisher = "Springer Nature",

address = "United States",

}

Banach, R 2008, UseCase-wise development: Retrenchment for event-B. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 5238, Springer Nature, pp. 167-180, 11th International Symposium on Recent Advances in Intrusion Detection, RAID 2008, London, 1/07/08. https://doi.org/10.1007/978-3-540-87603-8_14

TY - GEN

T1 - UseCase-wise development: Retrenchment for event-B

AU - Banach, Richard

N1 - British Comp Soc, Facs Nokia praxis Banach, Richard 16 BERLIN BIJ68

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

KW - Event-B

KW - Incremental Development

KW - Refinement

KW - Retrenchment

KW - Tower Pattern

KW - UseCase-wise development

U2 - 10.1007/978-3-540-87603-8_14

DO - 10.1007/978-3-540-87603-8_14

M3 - Conference contribution

SN - 3540876022

SN - 9783540876021

VL - 5238

SP - 167

EP - 180

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

PB - Springer Nature

T2 - 11th International Symposium on Recent Advances in Intrusion Detection, RAID 2008

Y2 - 1 July 2008

ER -

UseCase-wise development: Retrenchment for event-B

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this