UC-B: Use case modelling with Event-B

Rajiv Murali; Andrew Ireland; Gudmund Grov

doi:10.1007/978-3-319-33600-8_24

UC-B: Use case modelling with Event-B

Rajiv Murali, Andrew Ireland, Gudmund Grov

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

2 Citations (Scopus)

190 Downloads (Pure)

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 language	English
Title of host publication	Abstract State Machines, Alloy, B, TLA, VDM, and Z
Subtitle of host publication	5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings
Editors	Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, Miklos Biro
Publisher	Springer
Pages	297-302
Number of pages	6
ISBN (Electronic)	9783319336008
ISBN (Print)	9783319335995
DOIs	https://doi.org/10.1007/978-3-319-33600-8_24
Publication status	Published - 2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer International Publishing
Volume	9675
ISSN (Print)	0302-9743

Access to Document

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

Download pdf
The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-33600-8_24
Accepted author manuscript, 1.76 MBLicence: All Rights Reserved

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. https://doi.org/10.1007/978-3-319-33600-8_24

@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",

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",

}

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, 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, 2016. p. 297-302 (Lecture Notes in Computer Science; Vol. 9675).

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

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

ER -

UC-B: Use case modelling with Event-B

Abstract

Publication series

Access to Document

Fingerprint

Cite this