Eindhoven University of Technology (THE NETHERLANDS)
Philips Healthcare (THE NETHERLANDS)
Box Structure Development Method
CADP (Construction and Analysis of Distributed Processes)
78,088,550 states and 122,354,296 transitions
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:
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.
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
Department of Mathematics and Computer Science
Technische Universiteit Eindhoven
Den Dolech 2
PO Box 513
5600 MB Eindhoven
Tel: +31 (0)40 247 5035
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|