A rigorous approach to combining use case modelling and accident scenarios

Rajiv Murali, Andrew Ireland, Gudmund Grov

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

4 Citations (Scopus)
21 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 languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings
EditorsKlaus Havelund, Gerard Holzmann, Rajeev Joshi
PublisherSpringer
Pages263-278
Number of pages16
Volume9058
ISBN (Electronic)9783319175249
ISBN (Print)9783319175232
DOIs
Publication statusPublished - 2015
Event7th International Symposium on NASA Formal Methods - Pasadena, United States
Duration: 27 Apr 201529 Apr 2015

Publication series

NameLecture Notes in Computer Science
Volume9058
ISSN (Print)0302-9743

Conference

Conference7th International Symposium on NASA Formal Methods
Abbreviated titleNFM 2015
CountryUnited States
CityPasadena
Period27/04/1529/04/15

Keywords

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

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'A rigorous approach to combining use case modelling and accident scenarios'. Together they form a unique fingerprint.

  • 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