Formal Development of Control Software in the Medical Systems Domain

Organisation:	Eindhoven University of Technology (THE NETHERLANDS) Philips Healthcare (THE NETHERLANDS)
Method:	Box Structure Development Method CSP
Tools used:	FDR2 mCRL2 CADP (Construction and Analysis of Distributed Processes)
Domain:	Medical Systems.
Period:	2012
Size:	78,088,550 states and 122,354,296 transitions
Description:	Philips Healthcare develops a number of highly sophisticated medical systems, used for various clinical applications. One of these systems is the interventional X-ray system, which is used for minimally invasive surgeries. The system includes a number of graphical user interfaces, used for managing patients’ personal data, exam, and X-ray details. It also comprises a number of motorized movable parts such as the table where patients can lay and the stand where the X-ray generator and the image detector are fixed. Furthermore, the system contains a number of PCs and devices hosting the software that controls the entire system. Since the healthcare domain is quickly evolving, this requires a flexible software architecture that can be easily extended and maintained without the need of constructing the software from scratch. Philips Healthcare is gradually shifting to a component-based architecture with formally specified and verified interfaces. New components are developed according to this paradigm, and existing parts are gradually replaced by components with well-defined formal interfaces. This component-based development approach is based on a formal approach called Analytical Software Design (ASD). The aim of using the ASD approach at Philips Healthcare is to build high quality components that are mathematically verified at the design phase by eliminating defects as early as possible in the development life cycle, and thus reducing the effort and shortening the time devoted to integration and testing. This work is concerned with evaluating the use of the ASD formal techniques in industry, and investigating whether the use of the techniques resulted in better quality software compared to traditional development. It details in depth the experiences and the challenges encountered during the application of the techniques to the development of the iXR system, providing practical solutions to the encountered shortcomings. Two case-studies were considered: (1) a controller of a power distribution unit used to distribute electrical power and network signals to the PCs and the devices of the Xray system, and (2) a number of services deployed on the PCs of the X-ray system. Since not all specification guidelines can be modeled using the current ASD tool, the tools mCRL2, CSP/FDR2, and CADP were used instead for verification and formal refinement. After the specification of all models were created using the mCRL2 description language, the verification tasks were carried out. The mCRL2 tool set was used for verification and state space generation. The generated state spaces of all models were further analyzed using CADP for checking deadlocks, livelocks, illegals and proving refinements of designs against the external specification. In [Osaiweran-12] it is reported that: The last four refinement checks [observational, safety, tau*, and branching] were performed using CADP, which was the only tool supporting them.
Conclusions:	This work describes the effectiveness of applying a number of formal techniques to the development of industrial control software at Philips Healthcare. It is demonstrated 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 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.
Publications:	[Osaiweran-12] Ammar A. H. Osaiweran. "Formal Development of Control Software in the Medical Systems Domain". PhD thesis, Eindhoven University of Technology, December 2012. Available on-line at: http://alexandria.tue.nl/extra2/739209.pdf or from the CADP Web site in PDF or PostScript
Contact:	Ammar Osaiweran Department of Mathematics and Computer Science Technische Universiteit Eindhoven Den Dolech 2 PO Box 513 5600 MB Eindhoven The Netherlands Tel: +31 (0)40 247 5035 Email: a.a.h.osaiweran@tue.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page