A rigorous approach to combining use case modelling and accident scenarios

Rajiv Murali; Andrew Ireland; Gudmund Grov

doi:10.1007/978-3-319-17524-9_19

A rigorous approach to combining use case modelling and accident scenarios

Rajiv Murali^*, Andrew Ireland, Gudmund Grov

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

5 Citations (Scopus)

92 Downloads (Pure)

Abstract

We describe an approach to embedding a formal method within UML use case modelling. Moreover, we extend use case modelling to allow for the explicit representation of safety concerns. Our motivation comes from interaction with systems and safety engineers who routinely rely upon use case modelling during the early stages of defining and analysing system behaviours. Our chosen formal method is Event-B, which is refinement based and consequently has enabled us to exploit natural abstractions found within use case modelling. By underpinning informal use case modelling with Event-B, we are able to provide greater precision and formal assurance when reasoning about concerns identified by safety engineers as well as the subsequent changes made at the level of use case modelling. To achieve this we have extended use case modelling to include the notion of an accident case. Our approach is currently being implemented, and we have an initial prototype.

Original language	English
Title of host publication	NASA Formal Methods
Subtitle of host publication	7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings
Editors	Klaus Havelund, Gerard Holzmann, Rajeev Joshi
Publisher	Springer
Pages	263-278
Number of pages	16
Volume	9058
ISBN (Electronic)	9783319175249
ISBN (Print)	9783319175232
DOIs	https://doi.org/10.1007/978-3-319-17524-9_19
Publication status	Published - 2015
Event	7th International Symposium on NASA Formal Methods - Pasadena, United States Duration: 27 Apr 2015 → 29 Apr 2015

Publication series

Name	Lecture Notes in Computer Science
Volume	9058
ISSN (Print)	0302-9743

Conference

Conference	7th International Symposium on NASA Formal Methods
Abbreviated title	NFM 2015
Country/Territory	United States
City	Pasadena
Period	27/04/15 → 29/04/15

Keywords

Event-B
Formal modelling
Hazard analysis
Model based
Refinement
Use cases

ASJC Scopus subject areas

General Computer Science
Theoretical Computer Science

Access to Document

10.1007/978-3-319-17524-9_19

Download pdf
The final publication is available at Springer via https://link.springer.com/chapter/10.1007%2F978-3-319-17524-9_19
Accepted author manuscript, 1.11 MBLicence: All Rights Reserved

Cite this

Murali, R., Ireland, A., & Grov, G. (2015). A rigorous approach to combining use case modelling and accident scenarios. In K. Havelund, G. Holzmann, & R. Joshi (Eds.), NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings (Vol. 9058, pp. 263-278). (Lecture Notes in Computer Science; Vol. 9058). Springer. https://doi.org/10.1007/978-3-319-17524-9_19

Murali, Rajiv ; Ireland, Andrew ; Grov, Gudmund. / A rigorous approach to combining use case modelling and accident scenarios. NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings. editor / Klaus Havelund ; Gerard Holzmann ; Rajeev Joshi. Vol. 9058 Springer, 2015. pp. 263-278 (Lecture Notes in Computer Science).

@inbook{d2c1a171f9da4f699007c6c22f59c082,

title = "A rigorous approach to combining use case modelling and accident scenarios",

abstract = "We describe an approach to embedding a formal method within UML use case modelling. Moreover, we extend use case modelling to allow for the explicit representation of safety concerns. Our motivation comes from interaction with systems and safety engineers who routinely rely upon use case modelling during the early stages of defining and analysing system behaviours. Our chosen formal method is Event-B, which is refinement based and consequently has enabled us to exploit natural abstractions found within use case modelling. By underpinning informal use case modelling with Event-B, we are able to provide greater precision and formal assurance when reasoning about concerns identified by safety engineers as well as the subsequent changes made at the level of use case modelling. To achieve this we have extended use case modelling to include the notion of an accident case. Our approach is currently being implemented, and we have an initial prototype.",

keywords = "Event-B, Formal modelling, Hazard analysis, Model based, Refinement, Use cases",

author = "Rajiv Murali and Andrew Ireland and Gudmund Grov",

year = "2015",

doi = "10.1007/978-3-319-17524-9_19",

language = "English",

isbn = "9783319175232",

volume = "9058",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "263--278",

editor = "Havelund, {Klaus } and Holzmann, {Gerard } and Joshi, {Rajeev }",

booktitle = "NASA Formal Methods",

note = "7th International Symposium on NASA Formal Methods, NFM 2015 ; Conference date: 27-04-2015 Through 29-04-2015",

}

Murali, R, Ireland, A & Grov, G 2015, A rigorous approach to combining use case modelling and accident scenarios. in K Havelund, G Holzmann & R Joshi (eds), NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings. vol. 9058, Lecture Notes in Computer Science, vol. 9058, Springer, pp. 263-278, 7th International Symposium on NASA Formal Methods, Pasadena, United States, 27/04/15. https://doi.org/10.1007/978-3-319-17524-9_19

A rigorous approach to combining use case modelling and accident scenarios. / Murali, Rajiv; Ireland, Andrew; Grov, Gudmund.
NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings. ed. / Klaus Havelund; Gerard Holzmann; Rajeev Joshi. Vol. 9058 Springer, 2015. p. 263-278 (Lecture Notes in Computer Science; Vol. 9058).

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

TY - CHAP

T1 - A rigorous approach to combining use case modelling and accident scenarios

AU - Murali, Rajiv

AU - Ireland, Andrew

AU - Grov, Gudmund

PY - 2015

Y1 - 2015

N2 - We describe an approach to embedding a formal method within UML use case modelling. Moreover, we extend use case modelling to allow for the explicit representation of safety concerns. Our motivation comes from interaction with systems and safety engineers who routinely rely upon use case modelling during the early stages of defining and analysing system behaviours. Our chosen formal method is Event-B, which is refinement based and consequently has enabled us to exploit natural abstractions found within use case modelling. By underpinning informal use case modelling with Event-B, we are able to provide greater precision and formal assurance when reasoning about concerns identified by safety engineers as well as the subsequent changes made at the level of use case modelling. To achieve this we have extended use case modelling to include the notion of an accident case. Our approach is currently being implemented, and we have an initial prototype.

AB - We describe an approach to embedding a formal method within UML use case modelling. Moreover, we extend use case modelling to allow for the explicit representation of safety concerns. Our motivation comes from interaction with systems and safety engineers who routinely rely upon use case modelling during the early stages of defining and analysing system behaviours. Our chosen formal method is Event-B, which is refinement based and consequently has enabled us to exploit natural abstractions found within use case modelling. By underpinning informal use case modelling with Event-B, we are able to provide greater precision and formal assurance when reasoning about concerns identified by safety engineers as well as the subsequent changes made at the level of use case modelling. To achieve this we have extended use case modelling to include the notion of an accident case. Our approach is currently being implemented, and we have an initial prototype.

KW - Event-B

KW - Formal modelling

KW - Hazard analysis

KW - Model based

KW - Refinement

KW - Use cases

UR - http://www.scopus.com/inward/record.url?scp=84942581221&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-17524-9_19

DO - 10.1007/978-3-319-17524-9_19

M3 - Chapter (peer-reviewed)

AN - SCOPUS:84942581221

SN - 9783319175232

VL - 9058

T3 - Lecture Notes in Computer Science

SP - 263

EP - 278

BT - NASA Formal Methods

A2 - Havelund, Klaus

A2 - Holzmann, Gerard

A2 - Joshi, Rajeev

PB - Springer

T2 - 7th International Symposium on NASA Formal Methods

Y2 - 27 April 2015 through 29 April 2015

ER -

Murali R, Ireland A, Grov G. A rigorous approach to combining use case modelling and accident scenarios. In Havelund K, Holzmann G, Joshi R, editors, NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings. Vol. 9058. Springer. 2015. p. 263-278. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-17524-9_19

A rigorous approach to combining use case modelling and accident scenarios

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Andrew Ireland

Cite this

A rigorous approach to combining use case modelling and accident scenarios

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Profiles

Andrew Ireland

Cite this