With the advent of the electronic health record (EHR), the quality of patient care increased. Many hospitals are encouraging patients to voluntarily provide their own health status (patient health record, PHR) to be used by doctors when a healthcare encounter takes place. PHR information is usually provided through the help of medical devices (MDs). Blood pressure, heartbeat, body mass index, and body hydration can be continuously monitored by such devices. On the one hand, the information provided to the doctors can be very important to assisting the patient; on the other hand, the risk of having an unusable amount of data due to lack of data semantics is very high. For this reason, MD interoperability and security are two crucial concepts that each vendor must keep in mind. With the idea of helping device manufacturers, the authors present a rigorous approach for modeling and analyzing MDs based on formal methods.

The approach exploits Event-B and Rodin, two tools for system-level modeling and analysis. In particular, Event-B works well when various levels of abstraction are needed. In this case, the authors apply a four-step approach, including verification and validation. To detail the approach, a study on a hemodialysis MD is performed.

The idea of using Event-B and Rodin to support a rigorous approach to assist MD manufacturers is very interesting, and the example provided is very convincing. It would be very interesting to see an extended version of the paper, including a tutorial for MD manufacturers.