ROS Theses Repository

View Item 
  •   ROS Home
  • Mathematical & Computer Sciences
  • Doctoral Theses (Mathematical & Computer Sciences)
  • View Item
  •   ROS Home
  • Mathematical & Computer Sciences
  • Doctoral Theses (Mathematical & Computer Sciences)
  • View Item
  •   ROS Home
  • Mathematical & Computer Sciences
  • Doctoral Theses (Mathematical & Computer Sciences)
  • View Item
  • Admin
JavaScript is disabled for your browser. Some features of this site may not work without it.

A rigorous approach to combining use case modelling and accident scenarios

View/Open
MuraliR_0316_macs.pdf (4.705Mb)
Date
2016-03
Author
Murali, Rajiv
Metadata
Show full item record
Abstract
Nearly all serious accidents, in the past twenty years, in which software has been involved can be traced to requirements flaws. Accidents related to or involving safety-critical systems often lead to significant damage to life, property, and environment in which the systems operate. This thesis explores an extension to use case modelling that allows safety concerns to be modelled early in the systems development process. This 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 behaviour. The approach of embedded formal methods is adopted. That is, we use one discipline of use case modelling to guide the development of a formal model. This enables a greater precision and formal assurance when reasoning about concerns identified by system and safety engineers as well as the subsequent changes made at the level of use case modelling. The chosen formal method is Event-B, which is re nement based and has consequently enabled the approach to exploit a natural abstractions found within use case modelling. This abstraction of the problem found within use cases help introduce their behaviour into the Event-B model via step-wise re nement. The central ideas underlying this thesis are implemented in, UC-B, a tool support for modelling use cases on the Rodin platform (an eclipse-based development environment for Event-B). UC-B allows the specification of the use cases to be detailed with both informal and formal notation, and supports the automatic generation of an Event-B model given a formally specified use case. Several case studies of use cases with accident cases are provided, with their formalisation in Event-B supported by UC-B tool. An examination of the translation from use cases to Event-B model is discussed, along with the subsequent verification provided by Event-B to the use case model.
URI
http://hdl.handle.net/10399/3119
Collections
  • Doctoral Theses (Mathematical & Computer Sciences)

Browse

All of ROSCommunities & CollectionsBy Issue DateAuthorsTitlesThis CollectionBy Issue DateAuthorsTitles

ROS Administrator

LoginRegister
©Heriot-Watt University, Edinburgh, Scotland, UK EH14 4AS.

Maintained by the Library
Tel: +44 (0)131 451 3577
Library Email: libhelp@hw.ac.uk
ROS Email: open.access@hw.ac.uk

Scottish registered charity number: SC000278

  • About
  • Copyright
  • Accessibility
  • Policies
  • Privacy & Cookies
  • Feedback
AboutCopyright
AccessibilityPolicies
Privacy & Cookies
Feedback
 
©Heriot-Watt University, Edinburgh, Scotland, UK EH14 4AS.

Maintained by the Library
Tel: +44 (0)131 451 3577
Library Email: libhelp@hw.ac.uk
ROS Email: open.access@hw.ac.uk

Scottish registered charity number: SC000278

  • About
  • Copyright
  • Accessibility
  • Policies
  • Privacy & Cookies
  • Feedback
AboutCopyright
AccessibilityPolicies
Privacy & Cookies
Feedback