Research output: Contribution to Journal/Magazine › Journal article › peer-review
Research output: Contribution to Journal/Magazine › Journal article › peer-review
}
TY - JOUR
T1 - A Lease Based Hybrid Design Pattern for Proper-Temporal-Embedding of Wireless CPS Interlocking
AU - Tan, Feng
AU - Wang, Yufei
AU - Wang, Qixin
AU - Bu, Lei
AU - Suri, Neeraj
PY - 2015/10/1
Y1 - 2015/10/1
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 requires safety guarantees despite communication faults. This paper focuses on one important set of such safety rules: Proper-Temporal-Embedding (PTE), where distributed CPS entities must enter/leave risky states according to properly nested temporal pattern and certain duration spacing. Our solution introduces hybrid automata to formally describe and analyze CPS design patterns. We propose a novel leasing based design pattern, along with closed-form configuration constraints, to guarantee PTE safety rules under arbitrary wireless communication faults. We propose a formal procedure to transform the design pattern hybrid automata into specific wireless CPS designs. This procedure can effectively isolate physical world parameters from affecting the PTE safety of the resultant specific designs. We conduct two wireless CPS case studies, one on medicine and the other on control, to show that the resulted system is safe against communication failures. We also compare our approach with a polling based approach. Both approaches support PTE under arbitrary communication failures. The polling approach performs better under severely adverse wireless medium conditions; while ours performs better under benign or moderately adverse wireless medium conditions.
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 requires safety guarantees despite communication faults. This paper focuses on one important set of such safety rules: Proper-Temporal-Embedding (PTE), where distributed CPS entities must enter/leave risky states according to properly nested temporal pattern and certain duration spacing. Our solution introduces hybrid automata to formally describe and analyze CPS design patterns. We propose a novel leasing based design pattern, along with closed-form configuration constraints, to guarantee PTE safety rules under arbitrary wireless communication faults. We propose a formal procedure to transform the design pattern hybrid automata into specific wireless CPS designs. This procedure can effectively isolate physical world parameters from affecting the PTE safety of the resultant specific designs. We conduct two wireless CPS case studies, one on medicine and the other on control, to show that the resulted system is safe against communication failures. We also compare our approach with a polling based approach. Both approaches support PTE under arbitrary communication failures. The polling approach performs better under severely adverse wireless medium conditions; while ours performs better under benign or moderately adverse wireless medium conditions.
KW - Automata
KW - Base stations
KW - Computers
KW - Lasers
KW - Pistons
KW - Safety
KW - Wireless communication
U2 - 10.1109/TPDS.2014.2358224
DO - 10.1109/TPDS.2014.2358224
M3 - Journal article
AN - SCOPUS:84961771759
VL - 26
SP - 2630
EP - 2642
JO - IEEE Transactions on Parallel and Distributed Systems
JF - IEEE Transactions on Parallel and Distributed Systems
SN - 1045-9219
IS - 10
M1 - 6898840
ER -