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.
|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|
|Number of pages||6|
|Publication status||Published - 2016|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer International Publishing|