A Methodology for integration of formal methods in a healthcare case study

Luigia Petre; Elena Troubitsyna; Marina Walden; Pontus Boström; Niklas Engblom; Micaela Jansson

A Methodology for integration of formal methods in a healthcare case study

Luigia Petre, Elena Troubitsyna, Marina Walden, Pontus Boström, Niklas Engblom, Micaela Jansson

Research output: Book/Journal/Report › Commissioned report › Professional

31 Downloads (Pure)

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.

The work has been done within the EU-project MATISSE - Methodologies and Technologies for Industrial Strength Systems Engineering (IST-1999-11435, http://www.matisse.qinetiq.com/).

Original language	English
Publisher	Turku Centre for Computer Science (TUCS)
Number of pages	64
ISBN (Print)	952-12-0939-9
Publication status	Published - 2001
MoE publication type	D4 Published development or research report or study

Publication series

Name	TUCS Technical Reports
Volume	436

Access to Document

TR436Final published version, 6.03 MB

MATISSE: Methodologies and Technologies for Industrial Strength Systems Engineering (IST-1999-11435) (EU-project)
Walden, M. (Co-Principal Investigator), Sere, K. (Principal Investigator), Troubitsyna, E. (Co-Principal Investigator), Petre, L. (Co-Investigator), Boström, P. (Co-Investigator), Tsiopoulos, L. (Co-Investigator), Jansson, M. (Co-Investigator) & Engblom, N. (Co-Investigator)
01/05/00 → 28/02/03
Project: EU

Cite this

@book{7d1c7567d96146498b91f77b78acd16e,

title = "A Methodology for integration of formal methods in a healthcare case study",

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.The work has been done within the EU-project MATISSE - Methodologies and Technologies for Industrial Strength Systems Engineering (IST-1999-11435, http://www.matisse.qinetiq.com/).",

author = "Luigia Petre and Elena Troubitsyna and Marina Walden and Pontus Bostr{\"o}m and Niklas Engblom and Micaela Jansson",

note = "TUCS Technical Report No 436, December 2001",

year = "2001",

language = "English",

isbn = "952-12-0939-9",

series = "TUCS Technical Reports",

publisher = "Turku Centre for Computer Science (TUCS)",

}

TY - BOOK

T1 - A Methodology for integration of formal methods in a healthcare case study

AU - Petre, Luigia

AU - Troubitsyna, Elena

AU - Walden, Marina

AU - Boström, Pontus

AU - Engblom, Niklas

AU - Jansson, Micaela

N1 - TUCS Technical Report No 436, December 2001

PY - 2001

Y1 - 2001

N2 - 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.The work has been done within the EU-project MATISSE - Methodologies and Technologies for Industrial Strength Systems Engineering (IST-1999-11435, http://www.matisse.qinetiq.com/).

AB - 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.The work has been done within the EU-project MATISSE - Methodologies and Technologies for Industrial Strength Systems Engineering (IST-1999-11435, http://www.matisse.qinetiq.com/).

M3 - Commissioned report

SN - 952-12-0939-9

T3 - TUCS Technical Reports

BT - A Methodology for integration of formal methods in a healthcare case study

PB - Turku Centre for Computer Science (TUCS)

ER -

A Methodology for integration of formal methods in a healthcare case study

Abstract

Publication series

Access to Document

Fingerprint

Projects

MATISSE: Methodologies and Technologies for Industrial Strength Systems Engineering (IST-1999-11435) (EU-project)

Cite this