Where academic tradition
meets the exciting future

A Methodology for Integration of Formal Methods in a Healthcare Case Study

Luigia Petre, Elena Troubitsyna, Marina Waldén, Pontus Boström, Niklas Engblom, Micaela Jansson, A Methodology for Integration of Formal Methods in a Healthcare Case Study. TUCS Technical Reports 436, Turku Centre for Computer Science, 2001.

Abstract:

When developing safety-critical systems, it is necessary to satisfy not
only functional requirements defining the set of tasks to be performed by the
system, but also safety requirements describing the characteristics the
system should possess in order to ensure proper safety. Reliability is, as well,
an acute issue in the development of safety-critical systems. Enhancement
of safety and reliability can be achieved by applying formal methods, while
complexity of large systems can be mastered using a graphical language for
modelling, e.g., UML. Here we introduce a UML-based development process
that incorporates safety analysis and provides a logical interface to a formal
refinement based development in B-action systems. The tools associated
with the B Method provide a good mechanised support for proving the correctness
of the development within B-action systems. We show the feasibility of our
development process within a healthcare case study where we develop a
safety-critical drug discovery system.

Files:

Abstract in PDF-format

BibTeX entry:

@TECHREPORT{tPeTrWaBoEnJa01a,
  title = {A Methodology for Integration of Formal Methods in a Healthcare Case Study},
  author = {Petre, Luigia and Troubitsyna, Elena and Waldén, Marina and Boström, Pontus and Engblom, Niklas and Jansson, Micaela},
  number = {436},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2001},
  keywords = {Formal Methods, Safety Analysis, UML, Action Systems, the B Method},
}

Edit publication