Transforming Medical Best Practice Guidelines to Executable and Verifiable Statechart Models

Improving effectiveness and safety of patient care is an ultimate objective for medical cyber- physical systems. However, the existing medical best practice guidelines in hospital handbooks are often lengthy and difficult for medical staff to remember and apply clinically. Statechart is a widely used model in designing complex systems and enables rapid prototyping and clinical validation with medical doctors. However, clinical validation is often not adequate for guaranteeing the correctness and safety of medical cyber-physical systems, and formal verification is required. The paper presents an approach that transforms medical best practice guidelines to verifiable statechart models and supports both clinical validation in collaboration with medical doctors and formal verification. In particular, we use an open source statechart tool Yakindu to model best practice guidelines and use the statechart to interact with doctors for validating the model correctness. The statechart model is then automatically transformed to a verifiable formal model, such as timed automata, so that existing formal verification tool, such as UPPAAL, can be used to verify required safety properties. The approach also provides the ability to trace back to the paths in the statechart model (Yakindu model) when a specific property in its associated formal model (UPPAAL model) fails. A cardiac arrest scenario is used as a case study to validate the proposed approach. The tool is available on our website www.cs.iit.edu/~code/software/Y2U.