Model checking the properties of ISO/IEEE 11073-20601:2016 standard-based communication protocol for personal health device

Engineering of medical informatics systems is a complex work because it is at the intersection of several critical domains, among which medicine, computer science, electrical engineering to mention just a few. One critical aspect of such systems is the interoperability of the different components. One key solution for the interoperability is the creation of good standards that will assure the interchange of data between products of several vendors and domains - medical devices, medical information systems, medical data, etc. In this paper a formal analysis of the ISO/IEEE 11073 -20601: 2016 Draft Standard for Health informatics - Personal health device communication - Application profile - Optimized exchange protocol is described. This family of standards specifies the communication between devices that can be agents (weighing scales, spirometers) which measure health related data and managers (laptop, smartphone etc.) that collect the information and can display or forward it. First the protocol was modeled in Promela and then the model was checked manually and also using the Spin tool that performed an automated check. The results revealed issues which can cause deadlocks. However, these issues appeared in exceptional workflows, the normal flow being designed well. This highlights the methodology of developing such protocols: concentration on normal, intended behaviors without dealing with exceptional behaviors. Using formal models can reveal problems with exceptional behaviors. The results and proposed solutions were reported to the IEEE 1073 working group and will be integrated in the standard.