Please use this identifier to cite or link to this item:
http://hdl.handle.net/10397/5576
DC Field | Value | Language |
---|---|---|
dc.contributor | Department of Computing | - |
dc.creator | Li, T | - |
dc.creator | Tan, F | - |
dc.creator | Wang, Q | - |
dc.creator | Bu, L | - |
dc.creator | Cao, J | - |
dc.creator | Liu, X | - |
dc.date.accessioned | 2014-12-11T08:23:23Z | - |
dc.date.available | 2014-12-11T08:23:23Z | - |
dc.identifier.isbn | 978-1-4673-1537-1 | - |
dc.identifier.uri | http://hdl.handle.net/10397/5576 | - |
dc.language.iso | en | en_US |
dc.publisher | IEEE Computer Society | en_US |
dc.rights | © 2012 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. | en_US |
dc.subject | Biomedical equipment | en_US |
dc.subject | Formal verification | en_US |
dc.subject | Object-oriented methods | en_US |
dc.title | From offline toward real-time : a hybrid systems model checking and CPS co-design approach for medical device plug-and-play (MDPnP) | en_US |
dc.type | Conference Paper | en_US |
dc.description.otherinformation | Author name used in this manuscript: Jian-nong Cao | en_US |
dc.description.otherinformation | Refereed conference paper | en_US |
dc.identifier.doi | 10.1109/ICCPS.2012.10 | - |
dcterms.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: i) there are no good offline differential equation based models for many human body parameters, ii) 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., long-run) future behavior to online hybrid systems model checking of time-bounded (i.e., 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 co-design issue. We propose two sets of system co-design 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 co-design. | - |
dcterms.accessRights | open access | en_US |
dcterms.bibliographicCitation | Proceedings 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, ICCPS 2012, 17-19 April 2012, p.13-22 | - |
dcterms.issued | 2012-04 | - |
dc.identifier.scopus | 2-s2.0-84861486764 | - |
dc.identifier.rosgroupid | r61315 | - |
dc.description.ros | 2011-2012 > Academic research: refereed > Refereed conference paper | - |
dc.description.oa | Accepted Manuscript | en_US |
dc.identifier.FolderNumber | OA_IR/PIRA | en_US |
dc.description.pubStatus | Published | en_US |
Appears in Collections: | Conference Paper |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
ICCPS2012.pdf | Pre-published version | 1.08 MB | Adobe PDF | View/Open |
Page views
266
Last Week
1
1
Last month
Citations as of Apr 14, 2024
Downloads
326
Citations as of Apr 14, 2024
SCOPUSTM
Citations
25
Last Week
0
0
Last month
0
0
Citations as of Apr 19, 2024
WEB OF SCIENCETM
Citations
23
Last Week
0
0
Last month
0
0
Citations as of Apr 18, 2024
Google ScholarTM
Check
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.