The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - March (2014 vol.25)
pp: 642-652
Tao Li , Hong Kong Polytechnic University, Hong Kong
Feng Tan , Hong Kong Polytechnic University, Hong Kong
Qixin Wang , Hong Kong Polytechnic University, Hong Kong
Lei Bu , Nanjing University, Nanjing
Jian-Nong Cao , Hong Kong Polytechnic University, Hong Kong
Xue Liu , McGill University, Montreal
ABSTRACT
Hybrid systems model checking is a great success in guaranteeing the safety of computerized control cyber-physical systems (CPS). However, when applying hybrid systems model checking to Medical Device Plug-and-Play (MDPnP) CPS, we encounter two challenges due to the complexity of human body: 1) there are no good offline differential equation-based models for many human body parameters; 2) the complexity of human body can result in many variables, complicating the system model. In an attempt to address the challenges, we propose to alter the traditional approach of offline hybrid systems model checking of time-unbounded (i.e., infinite horizon, a.k.a., long run) future behavior to online hybrid systems model checking of time-bounded (i.e., finite horizon, a.k.a., short run) future behavior. According to this proposal, online model checking runs as a real-time task to prevent faults. To meet the real-time requirements, certain design patterns must be followed, which brings up the codesign issue. We propose two sets of system codesign patterns for hard real time and soft real time, respectively. To evaluate our proposals, a case study on laser tracheotomy MDPnP is carried out. The study shows the necessity of online model checking. Furthermore, test results based on real-world human subject trace show the feasibility and effectiveness of our proposed codesign.
INDEX TERMS
Automata, Laser modes, Model checking, Biological system modeling, Blood, Safety,model checking, Cyber-physical systems, real-time, medical, hybrid systems
CITATION
Tao Li, Feng Tan, Qixin Wang, Lei Bu, Jian-Nong Cao, Xue Liu, "From Offline toward Real Time: A Hybrid Systems Model Checking and CPS Codesign Approach for Medical Device Plug-and-Play Collaborations", IEEE Transactions on Parallel & Distributed Systems, vol.25, no. 3, pp. 642-652, March 2014, doi:10.1109/TPDS.2013.50
REFERENCES
[1] Medical Device Plug-and-Play (MDPnP), http:/www.mdpnp.org. 2013.
[2] L. Sha et al., "Cyber-Physical Systems: A New Frontier," Machine Learning in Cyber Trust: Security, Privacy, and Reliability. Springer, 2009.
[3] C. Baier et al., Principles of Model Checking. MIT Press, 2008.
[4] P. Tabuada, Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, 2009.
[5] P.J. Antsaklis and X.D. Koutsoukos, "Hybrid Systems: Review and Recent Progress," Software-Enabled Control: Information Technology for Dynamical Systems. IEEE Press, pp. 273-298, 2003.
[6] I. Lee and O. Sokolsky, "Medical Cyber Physical Systems," Proc. 47th ACM/IEEE Design Automation Conference (DAC '10), 2010.
[7] C. Kim et al., "A Framework for the Safe Interoperability of Medical Devices in the Presence Of Network Failures," Proc. 1st ACM/IEEE Int'l Conf. Cyber-Physical Systems (ICCPS '10), Apr. 2010.
[8] J.A. Grass, "Patient-Controlled Analgesia," Anesthesia and Analgesia, vol. 101, no. 5S, pp. S44-S61, Nov. 2005.
[9] J.X. Mazoit, K. Butscher, and K. Samii, "Morphine in Postoperative Patients: Pharmacokinetics and Pharmacodynamics of Metabolites," Anesthesia and Analgesia, vol. 105, no. 1, pp. 70-78, 2007.
[10] "Medical Devices and Medical Systems - Essential Safety Requirements for Equipment Comprising the Patient-Centric Integrated Clinical Environment (ICE), Part 1: General Requirements and Conceptual Model," no. STAM F2761-2009, 2009.
[11] T. Li et al., "From Offline toward Real-Time: A Hybrid Systems Model Checking and CPS Co-Design Approach for Medical Device Plug-and-Play (MDPnP)," Proc. IEEE/ACM Third Int'l Conf. Cyber-Physical Systems (ICCPS '12), pp. 13-22, Apr. 2012.
[12] T. Li et al., "From Offline Long-Run to Online Short-Run: Exploring a New Approach of Hybrid Systems Model Checking for MDPnP," Proc. Joint Workshop High Confidence Medical Devices, Software, and Systems (HCMDSS) and Medical Device Plug-and-Play (MDPnP) Interoperability, Apr. 2011.
[13] L. Bu et al., "Toward Online Hybrid Systems Model Checking of Cyber-Physical Systems Time-Bounded Short-Run Behavior," Proc. IEEE/ACM Third Int'l Conf. Cyber-Physical Systems (ICCPS '11) Work-in-Progress Session, Apr. 2011.
[14] R. Alur et al., "Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems," Hybrid Systems, vol. 736, pp. 209-229, 1992.
[15] R. Alur et al., "Automatic Symbolic Verification of Embedded Systems," IEEE Trans. Software Eng., vol. 22, no. 3, pp. 181-201, Mar. 1996.
[16] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, "Hytech: a Model Checker for Hybrid Systems," Int'l J. Software Tools for Technology Transfer, vol. 1, nos. 1-2, pp. 110-122, 1997.
[17] J.A. Dorsch and S.E. Dorsch, Understanding Anesthesia Equipment, fifth ed. Lippincott Williams and Wilkins, 2007.
[18] G. Frehse, "PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech," Proc. Eigth Int'l Conf. Hybrid Systems: Computation and Control (HSCC '05), pp. 258-273, 2005.
[19] Nonin 9843 Oximeter/Co2 Detector, http:/www.nonin.com, 2013.
[20] M.J. Moran et al., Fundamentals of Eng. Thermodynamics. Wiley, 2003.
[21] O. Roux and V. Rusu, "Uniformity for the Decidability of Hybrid Automata," Static Analysis, vol. 1145, pp. 301-316, 1996.
[22] T. Li et al., from Offline toward Real-Time: A Hybrid Systems Model Checking and CPS Co-Design Approach for Medical Device Plug-and-Play, technical report Appendices, http:/www.comp.polyu. edu.hk/, 2013.
[23] F. Brunicardi et al., Principles of Surgery. McGraw-Hill, Sept. 2009.
[24] PhysioNet: the Research Resource for Complex Physiologic Signals, http:/www.physionet.org, 2013.
[25] Y. Wang et al., "WiCop: Engineering WiFi Temporal White-Spaces for Safe Operations of Wireless Body Area Networks in Medical Applications," Proc. IEEE 32nd Real-Time Systems Symp. (RTSS '11), pp. 170-179, 2011.
[26] J. Huang et al., "Beyond Co-Existence: Exploiting WiFi White Space for ZigBee Performance Assurance," Proc. 18th IEEE Int'l Conf. Network Protocols (ICNP '10), pp. 305-314, Oct. 2010.
[27] Q. Wang et al., "Building Robust Wireless LAN for Industrial Control with the DSSS-CDMA Cell Phone Network Paradigm," IEEE Trans. Mobile Computing, vol. 6, no. 6, pp. 706-719, June 2007.
[28] S. Baker et al., "Medical-Grade, Mission-Critical Wireless Networks," IEEE Eng. in Medicine and Biology Magazine, vol. 27, no. 2, pp. 86-95, Mar./Apr. 2008.
[29] B. Finkbeiner et al., "Collecting Statistics over Runtime Executions," Electronic Notes in Theoretical Computer Science, vol. 70, no. 4, pp. 36-54, 2002.
[30] K. Sen, G. Rosu, and G. Agha, "Online Efficient Predictive Safety Analysis of Multithreaded Programs," Proc. 10th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS' 04), pp. 123-138, 2004.
[31] A. Easwaran et al., "Steering of Discrete Event Systems: Control Theory Approach," Proc. Int'l Workshop Runtime Verification, 2006.
[32] Z. Qi et al., "A Hybrid Model Checking and Runtime Monitoring Method for C++ Web Services," Proc. Int'l Joint Conf. INC, IMS, and IDC, 2009.
[33] D. Harel, H. Kugler, R. Marelly, and A. Pnueli, "Smart Play-Out of Behavioral Requirements," Proc. Fourth Int'l Conf. Formal Methods in Computer-Aided Design (FMCAD '02), pp. 378-398, 2002.
[34] G. Sauterand et al., "Lightweight Hybrid Model Checking Facilitating Online Prediction of Temporal Properties," Proc. 21st Nordic Workshop Programming Theory, (NWPT '09), pp. 20-22, 2009.
[35] C. Li, M. Nagasaki, C.H. Koh, and S. Miyano, "Online Model Checking Approach Based Parameter Estimation to a Neuronal Fate Decision Simulation Model in Caenorhabditis Elegans with Hybrid Functional Petri Net with Extension," Molecular BioSystems, no. 7, pp. 1576-1592, 2011.
[36] K.G. Larsen, M. Mikucionis, and B. Nielsen, "Uppaal Tron User Manual," 2007.
[37] Robby et al., "Bogor: An Extensible and Highly-Modular Software Model Checking Framework," Proc. Nineth European Software Eng. Conf. (ESEC/FSE '11), 2003.
[38] E. Bartocci et al., "Cellexcite: An Efficient Simulation Environment for Excitable Cells," BMC Bioinformatics, vol. 9, no. 2, pp. 1-13, Mar. 2008.
[39] J. Ko et al., "Wireless Sensor Networks for Healthcare," Proc. IEEE, vol. 98, no. 1, pp. 1947-1960, Nov. 2010.
[40] A. King et al., "An Open Test Bed for Medical Device Integration and Coordination," Proc. 31st Int'l Conf. Software Eng. (ICSE '09), May 2009.
[41] R. Alur and G. Weiss, "RTComposer: A Framework for Real-Time Components with Scheduling Interfaces," Proc. Eigth ACM Int'l Conf. Embedded Software (EMSOFT '08), pp. 159-168, 2008.
[42] Y. Krishnamurthy et al., "The Design and Implementation Of Real-Time Corba 2.0: Dynamic Scheduling in Tao," Proc. IEEE 10th Real-Time and Embedded Technology and Applications Symp. (RTAS '04), 2004.
38 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool