UC-B: Use case modelling with Event-B

Rajiv Murali, Andrew Ireland, Gudmund Grov

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

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
PublisherSpringer International Publishing
Pages297-302
Number of pages6
ISBN (Electronic)9783319336008
ISBN (Print)9783319335995
DOIs
Publication statusPublished - 2016

Publication series

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

Fingerprint

Specifications

Cite this

Murali, R., Ireland, A., & Grov, G. (2016). UC-B: Use case modelling with Event-B. In M. Butler, K-D. Schewe, A. Mashkoor, & M. Biro (Eds.), Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings (pp. 297-302). (Lecture Notes in Computer Science; Vol. 9675). Springer International Publishing. https://doi.org/10.1007/978-3-319-33600-8_24
Murali, Rajiv ; Ireland, Andrew ; Grov, Gudmund. / UC-B: Use case modelling with Event-B. Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. editor / Michael Butler ; Klaus-Dieter Schewe ; Atif Mashkoor ; Miklos Biro. Springer International Publishing, 2016. pp. 297-302 (Lecture Notes in Computer Science).
@inbook{e3a5b11688ed432e9c036ccb9ce858d5,
title = "UC-B: Use case modelling with Event-B",
abstract = "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.",
author = "Rajiv Murali and Andrew Ireland and Gudmund Grov",
year = "2016",
doi = "10.1007/978-3-319-33600-8_24",
language = "English",
isbn = "9783319335995",
series = "Lecture Notes in Computer Science",
publisher = "Springer International Publishing",
pages = "297--302",
editor = "Michael Butler and Klaus-Dieter Schewe and Atif Mashkoor and Miklos Biro",
booktitle = "Abstract State Machines, Alloy, B, TLA, VDM, and Z",
address = "Switzerland",

}

Murali, R, Ireland, A & Grov, G 2016, UC-B: Use case modelling with Event-B. in M Butler, K-D Schewe, A Mashkoor & M Biro (eds), Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9675, Springer International Publishing, pp. 297-302. https://doi.org/10.1007/978-3-319-33600-8_24

UC-B: Use case modelling with Event-B. / Murali, Rajiv; Ireland, Andrew; Grov, Gudmund.

Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. ed. / Michael Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklos Biro. Springer International Publishing, 2016. p. 297-302 (Lecture Notes in Computer Science; Vol. 9675).

Research output: Chapter in Book/Report/Conference proceedingChapter

TY - CHAP

T1 - UC-B: Use case modelling with Event-B

AU - Murali, Rajiv

AU - Ireland, Andrew

AU - Grov, Gudmund

PY - 2016

Y1 - 2016

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

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

U2 - 10.1007/978-3-319-33600-8_24

DO - 10.1007/978-3-319-33600-8_24

M3 - Chapter

SN - 9783319335995

T3 - Lecture Notes in Computer Science

SP - 297

EP - 302

BT - Abstract State Machines, Alloy, B, TLA, VDM, and Z

A2 - Butler, Michael

A2 - Schewe, Klaus-Dieter

A2 - Mashkoor, Atif

A2 - Biro, Miklos

PB - Springer International Publishing

ER -

Murali R, Ireland A, Grov G. UC-B: Use case modelling with Event-B. In Butler M, Schewe K-D, Mashkoor A, Biro M, editors, Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. Springer International Publishing. 2016. p. 297-302. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-33600-8_24