TY - GEN
T1 - Provably correct design of observations for fault detection with privacy preservation
AU - Xu, Zhe
AU - Saha, Sayan
AU - Julius, Agung
N1 - Funding Information:
ACKNOWLEDGMENT The authors would like to thank Dr. Yi Deng for helpful discussions. The authors would also like to thank Charles C. Okaeme and Dr. Sandipan Mishra for introducing us to the smart building testbed. This research was partially supported by the National Science Foundation through grants CNS-1218109, CNS-1550029 and CNS-1618369.
Publisher Copyright:
© 2017 IEEE.
PY - 2017/6/28
Y1 - 2017/6/28
N2 - During the operation of complex cyber-physical systems, detection of faults needs to be performed using limited state information for practicality and privacy concerns. While a well-designed observation can distinguish a faulty behavior from the normal behavior, it can also represent the action of hiding some of the state information or discrete mode transitions. In this paper, we present a framework for constructing the observation maps in the form of metric temporal logic (MTL) formulae that can be formally proven to detect fault in a switched system while preserving certain privacy conditions. We simulate finitely many nominal trajectories and use the robustness tubes around the simulated trajectories to cover the infinite trajectories that constitute the system behavior. Thus the inferred MTL formulae from the simulated trajectories can be used for classifying the system behaviors in a provably correct fashion. We implement our approach on the simulation model of a smart building testbed to detect the open window fault while preserving the privacy of the room occupancy.
AB - During the operation of complex cyber-physical systems, detection of faults needs to be performed using limited state information for practicality and privacy concerns. While a well-designed observation can distinguish a faulty behavior from the normal behavior, it can also represent the action of hiding some of the state information or discrete mode transitions. In this paper, we present a framework for constructing the observation maps in the form of metric temporal logic (MTL) formulae that can be formally proven to detect fault in a switched system while preserving certain privacy conditions. We simulate finitely many nominal trajectories and use the robustness tubes around the simulated trajectories to cover the infinite trajectories that constitute the system behavior. Thus the inferred MTL formulae from the simulated trajectories can be used for classifying the system behaviors in a provably correct fashion. We implement our approach on the simulation model of a smart building testbed to detect the open window fault while preserving the privacy of the room occupancy.
UR - http://www.scopus.com/inward/record.url?scp=85046124806&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85046124806&partnerID=8YFLogxK
U2 - 10.1109/CDC.2017.8264507
DO - 10.1109/CDC.2017.8264507
M3 - Conference contribution
AN - SCOPUS:85046124806
T3 - 2017 IEEE 56th Annual Conference on Decision and Control, CDC 2017
SP - 5620
EP - 5625
BT - 2017 IEEE 56th Annual Conference on Decision and Control, CDC 2017
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 56th IEEE Annual Conference on Decision and Control, CDC 2017
Y2 - 12 December 2017 through 15 December 2017
ER -