Formal development of control software in the medical systems domain

A.A.H. Osaiweran

    Research output: ThesisPhd Thesis 1 (Research TU/e / Graduation TU/e)

    251 Downloads (Pure)


    In this thesis we describe the effectiveness of applying a number of formal techniques to the development of industrial control software at Philips Healthcare. We demonstrate how these techniques were tightly incorporated to the industrial workflow and the issues encountered during the application. The work was established in an industrial context, dealing with real industrial projects and a real product concerning the development of interventional X-ray systems. The results are very conclusive in the sense that the used formal techniques could deliver substantially better quality code compared to the code developed in conventional development methods. Also, the results show that the productivity of the formally developed code is better than the productivity of code developed by projects at Philips Healthcare or projects reported worldwide. The thesis also includes a number of design and specification guidelines that assist constructing verifiable components using model checking. The guidelines were successful in designing and verifying a controller component developed at Philips Healthcare. Hence, the guidelines can provide an effective framework to design verifiable control components in industrial settings.
    Original languageEnglish
    QualificationDoctor of Philosophy
    Awarding Institution
    • Mathematics and Computer Science
    • Groote, Jan Friso, Promotor
    • Hooman, Jozef J.M., Promotor, External person
    Award date15 Dec 2012
    Place of PublicationEindhoven
    Print ISBNs978-90-386-3276-6
    Publication statusPublished - 2012


    Dive into the research topics of 'Formal development of control software in the medical systems domain'. Together they form a unique fingerprint.

    Cite this