Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Rigorous modeling and analysis of interoperable medical devices
Mashkoor A., Sametinger J.  MSM 2016 (Proceedings of the Modeling and Simulation in Medicine Symposium, Pasadena, CA, Apr 3-6, 2016)1-8.2016.Type:Proceedings
Date Reviewed: Aug 18 2016

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.

Reviewer:  Massimiliano Masi Review #: CR144697 (1611-0813)
Bookmark and Share
  Reviewer Selected
Featured Reviewer
 
 
Model Checking (D.2.4 ... )
 
 
Medical Information Systems (J.3 ... )
 
 
Model Validation And Analysis (I.6.4 )
 
Would you recommend this review?
yes
no
Other reviews under "Model Checking": Date
Systems and software verification: model-checking techniques and tools
B ., Bidoit M., Finkel A., Laroussinie F., Petit A., Petrucci L., Schnoebelen P., McKenzie P., Springer-Verlag New York, Inc., New York, NY, 1999.  190, Type: Book (9783540415237)
Sep 30 2002
Module checking
Kupferman O., Vardi M., Wolper P. Information and Computation 164(2): 322-344, 2001. Type: Article
Mar 1 2002
SMC: a symmetry-based model checker for verification of safety and liveness properties
Sistla A., Gyuris V., Emerson E. ACM Transactions on Software Engineering and Methodology 9(2): 133-166, 2000. Type: Article
Sep 1 2000
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy