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, 2012.

ABSTRACT

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.