Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
}
TY - GEN
T1 - Guaranteeing Proper-Temporal-Embedding safety rules in wireless CPS
T2 - A hybrid formal modeling approach
AU - Tan, F.
AU - Wang, Y.
AU - Wang, Q.
AU - Bu, L.
AU - Zheng, R.
AU - Suri, Neeraj
PY - 2013/6/24
Y1 - 2013/6/24
N2 - Cyber-Physical Systems (CPS) integrate discrete-time computing and continuous-time physical-world entities, which are often wirelessly interlinked. The use of wireless safety critical CPS (control, healthcare etc.) requires safety guarantees despite communication faults. This paper focuses on one important set of such safety rules: Proper-Temporal-Embedding (PTE). Our solution introduces hybrid automata to formally describe and analyze CPS design patterns. We propose a novel lease based design pattern, along with closed-form configuration constraints, to guarantee PTE safety rules under arbitrary wireless communication faults. We propose a formal methodology to transform the design pattern hybrid automata into specific wireless CPS designs. This methodology can effectively isolate physical world parameters from affecting the PTE safety of the resultant specific designs. We conduct a case study on laser tracheotomy wireless CPS to show that the resulting system is safe and can withstand communication disruptions. © 2013 IEEE.
AB - Cyber-Physical Systems (CPS) integrate discrete-time computing and continuous-time physical-world entities, which are often wirelessly interlinked. The use of wireless safety critical CPS (control, healthcare etc.) requires safety guarantees despite communication faults. This paper focuses on one important set of such safety rules: Proper-Temporal-Embedding (PTE). Our solution introduces hybrid automata to formally describe and analyze CPS design patterns. We propose a novel lease based design pattern, along with closed-form configuration constraints, to guarantee PTE safety rules under arbitrary wireless communication faults. We propose a formal methodology to transform the design pattern hybrid automata into specific wireless CPS designs. This methodology can effectively isolate physical world parameters from affecting the PTE safety of the resultant specific designs. We conduct a case study on laser tracheotomy wireless CPS to show that the resulting system is safe and can withstand communication disruptions. © 2013 IEEE.
KW - Configuration constraints
KW - Continuous-time
KW - Cyber-physical systems (CPS)
KW - Design Patterns
KW - Hybrid automatons
KW - Physical world
KW - Safety guarantees
KW - Wireless communications
KW - Communication
KW - Embedded systems
KW - Java programming language
KW - Wireless telecommunication systems
KW - Automata theory
U2 - 10.1109/DSN.2013.6575357
DO - 10.1109/DSN.2013.6575357
M3 - Conference contribution/Paper
SN - 9781467364713
BT - 2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)
PB - IEEE
ER -