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)

190 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
  • Department of 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

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

  • Cite this