| dc.description.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. | en_US |
