Data-Centered Runtime Verification of Wireless Medical Cyber-Physical System
Data-Centered Runtime Verification of Wireless Medical Cyber-Physical System
复制标题
DOI：
10.1109/tii.2016.2573762
复制
发表时间：
2017-08-01
影响因子：
12.3
通讯作者：
Sha, Lui
中科院分区：
文献类型：
--
作者：
Jiang, Yu;Song, Houbing;Sha, Lui
无线医疗信息物理系统在日常医疗实践中被广泛采用，无线医疗设备和传感器对大量数据进行采样，并将其传递给决策支持系统（DSSs）。许多基于文本的指南已被编码，用于DSS的工作流模拟，以根据收集到的数据实现医疗保健自动化。但对于一些复杂的、危及生命的疾病，迫切需要对这些数据中编码的一些复杂的时间属性进行自动严格的验证，这给目前基于仿真的DSS带来了新的挑战，而自动形式验证和实时数据分析的支持有限。在本文中，我们首次研究了基于实时数据的应用运行时验证来配合现有的决策支持系统。在提出的技术中，设计了一种用户友好的领域特定语言，称为DRTV，用于指定由医疗设备采样的重要实时数据和源自临床指南的时间属性。开发了数据采集和通信接口。然后，对于DRTV模型中描述的医疗实践场景，我们将自动生成事件序列和运行时属性验证器自动机。如果违反时间属性，将由正式验证者产生实时警告并传递给医疗DSS。我们已经使用DRTV来指定不同类型的医疗场景，并应用所提出的技术来辅助现有的无线医疗信息物理系统。实验结果表明，在预警检测方面，优于单纯使用DSS或人工检测，提高了医院临床医疗质量。
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.