Experiences with a Compositional Model Checker
in the Healthcare Domain
Jozef Hooman, Robert Huis in 't Veld, and Mathijs Schuts
Appeared in: Foundations of Health Information Engineering
and Systems (FHIES 2011),
LNCS 7151, pages 93-110, Springer-Verlag,
This paper describes the use of a formal method to support component-based development in the healthcare domain. The method is based on a commercial tool suite which combines formal modeling, compositional model checking, and code generation. The main approach of the tool suite will be explained and demonstrated from a user point of view. We report about experiences with this approach at the company Philips Healthcare for the design of control software for advanced interventional X-ray systems. This concerns formal interface definitions between the main system components and detailed design of control components.