TY - JOUR
T1 - Data-centered runtime verification of wireless medical cyber-physical system
AU - Jiang, Yu
AU - Song, Houbing
AU - Wang, Rui
AU - Gu, Ming
AU - Sun, Jiaguang
AU - Sha, Lui
N1 - Manuscript received March 3, 2016; revised May 8, 2016; accepted May 17, 2016. Date of publication May 27, 2016; date of current version August 1, 2017. This work was supported in part by the National Science Foundation (NSF) under Grant CNS 13-30077, Grant CNS 13-29886, and Grant CNS 15-45002, and in part by the National Science Foundation China (NSFC) under Grant 61303014. Paper no. TII-16-0255. (Corresponding author: R. Wang.) Y. Jiang is with the School of Software, Tsinghua University, Beijing 100084, China, also with the Beijing Advanced Innovation Center for Imaging Technology, Capital Normal University, Beijing 100048, China, and also with the Department of Computer Science, University of Illinois at Urbana–Champaign, Champaign, IL 61820 USA (e-mail: [email protected]).
PY - 2017/8
Y1 - 2017/8
N2 - Wireless medical cyber-physical systems are widely adopted in the daily practices of medicine, where huge amounts of data are sampled by the wireless medical devices and sensors, and is passed to the decision support systems (DSSs). Many text-based guidelines have been encoded for work-flow simulation of DSS to automate health care based on those collected data. But for some complex and life-critical diseases, it is highly desirable to automatically rigorously verify some complex temporal properties encoded in those data, which brings new challenges to current simulation-based DSS with limited support of automatical formal verification and real-time data analysis. In this paper, we conduct the first study on applying runtime verification to cooperate with current DSS based on real-time data. Within the proposed technique, a user-friendly domain specific language, named DRTV, is designed to specify vital real-time data sampled by medical devices and temporal properties originated from clinical guidelines. Some interfaces are developed for data acquisition and communication. Then, for medical practice scenarios described in DRTV model, we will automatically generate event sequences and runtime property verifier automata. If a temporal property violates, real-time warnings will be produced by the formal verifier and passed to medical DSS. We have used DRTV to specify different kinds of medical care scenarios and have applied the proposed technique to assist existing wireless medical cyber-physical system. As presented in experiment results, in terms of warning detection, it outperforms the only use of DSS or human inspection, and improves the quality of clinical health care of hospital.
AB - Wireless medical cyber-physical systems are widely adopted in the daily practices of medicine, where huge amounts of data are sampled by the wireless medical devices and sensors, and is passed to the decision support systems (DSSs). Many text-based guidelines have been encoded for work-flow simulation of DSS to automate health care based on those collected data. But for some complex and life-critical diseases, it is highly desirable to automatically rigorously verify some complex temporal properties encoded in those data, which brings new challenges to current simulation-based DSS with limited support of automatical formal verification and real-time data analysis. In this paper, we conduct the first study on applying runtime verification to cooperate with current DSS based on real-time data. Within the proposed technique, a user-friendly domain specific language, named DRTV, is designed to specify vital real-time data sampled by medical devices and temporal properties originated from clinical guidelines. Some interfaces are developed for data acquisition and communication. Then, for medical practice scenarios described in DRTV model, we will automatically generate event sequences and runtime property verifier automata. If a temporal property violates, real-time warnings will be produced by the formal verifier and passed to medical DSS. We have used DRTV to specify different kinds of medical care scenarios and have applied the proposed technique to assist existing wireless medical cyber-physical system. As presented in experiment results, in terms of warning detection, it outperforms the only use of DSS or human inspection, and improves the quality of clinical health care of hospital.
KW - Decision support system (DSS)
KW - real-time data
KW - runtime verification
KW - wireless medical cyber-physical system
UR - http://www.scopus.com/inward/record.url?scp=85029676612&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85029676612&partnerID=8YFLogxK
U2 - 10.1109/TII.2016.2573762
DO - 10.1109/TII.2016.2573762
M3 - Article
AN - SCOPUS:85029676612
SN - 1551-3203
VL - 13
SP - 1900
EP - 1909
JO - IEEE Transactions on Industrial Informatics
JF - IEEE Transactions on Industrial Informatics
IS - 4
M1 - 7480373
ER -