Paper Info
Title
Systematically Debugging IoT Control System Correctness for Building Automation.
Abstract
Advances and standards in Internet of Things (IoT) have simplified the realization of building automation. However, non-expert IoT users still lack tools that can help them to ensure the underlying control system correctness: user-programmable logics match the user intention. In fact, non-expert IoT users lack the necessary know-how of domain experts. This paper presents our experience in running a building automation service based on the Salus framework. Complementing efforts that simply verify the IoT control system correctness, Salus takes novel steps to tackle practical challenges in automated debugging of identified policy violations, for non-expert IoT users. First, Salus leverages formal methods to localize faulty user-programmable logics. Second, to debug these identified faults, Salus selectively transforms the control system logics into a set of parameterized equations, which can then be solved by popular model checking tools or SMT (Satisfiability Modulo Theories) solvers. Through office deployments, user studies, and public datasets, we demonstrate the usefulness of Salus in systematically debugging the correctness of IoT control systems for building automation.
Year
DOI
Venue
2016
10.1145/2993422.2993426
BuildSys@SenSys
Keywords
Field
DocType
policy verification,policy violation debugging,IoT
Parameterized complexity,Model checking,Software engineering,Computer science,Correctness,Building automation,Control system,Formal methods,Debugging,Satisfiability modulo theories,Distributed computing
Conference
Citations 
PageRank 
References 
14
0.65
26
Authors
8
Name
Order
Citations
PageRank
Chieh-Jan Mike Liang180443.13
Lei Bu218922.50
Zhao Li3140.65
Junbei Zhang4221.26
Shi Han529615.22
Börje Karlsson6788.21
Dongmei Zhang71439132.94
Feng Zhao84593455.17