UC-B: Use case modelling with Event-B

Rajiv Murali, Andrew Ireland, Gudmund Grov

Research output: Chapter in Book/Report/Conference proceedingChapter

2 Citations (Scopus)
148 Downloads (Pure)


Use cases are a popular but informal technique used to define and analyse system behaviour. We introduce UC-B a plug-in for the Rodin platform (Event-B tool) that supports the authoring and management of use case specifications with both informal and formal components. The formal component is based on Event-B's mathematical language. Once the behaviour of the use case is specified, UC-B automatically generates a corresponding Event-B model. The resulting model is then amenable to the Rodin verification tools that enable system level properties to be verified. By underpinning informal use case modelling with Event-B we are able to provide greater precision and formal assurance during the early stages of design.
Original languageEnglish
Title of host publicationAbstract State Machines, Alloy, B, TLA, VDM, and Z
Subtitle of host publication5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings
EditorsMichael Butler, Klaus-Dieter Schewe, Atif Mashkoor, Miklos Biro
Number of pages6
ISBN (Electronic)9783319336008
ISBN (Print)9783319335995
Publication statusPublished - 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
ISSN (Print)0302-9743


Dive into the research topics of 'UC-B: Use case modelling with Event-B'. Together they form a unique fingerprint.

Cite this