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/ReportCommissioned reportProfessional

    18 Downloads (Pure)


    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 languageEnglish
    PublisherTurku Centre for Computer Science (TUCS)
    Number of pages64
    ISBN (Print)952-12-0939-9
    Publication statusPublished - 2001
    MoE publication typeD4 Published development or research report or study

    Publication series

    NameTUCS Technical Reports


    Dive into the research topics of 'A Methodology for integration of formal methods in a healthcare case study'. Together they form a unique fingerprint.

    Cite this