Systematically Debugging IoT Control System Correctness for Building Automation
| Autor: | Chieh-Jan Mike Liang, Dongmei Zhang, Zhao Li, Shi Han, Feng Zhao, Lei Bu, Junbei Zhang, Börje F. Karlsson |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Model checking
Service (systems architecture) Correctness Computer science business.industry media_common.quotation_subject Distributed computing 020207 software engineering 02 engineering and technology Formal methods 020202 computer hardware & architecture Domain (software engineering) Debugging Satisfiability modulo theories 0202 electrical engineering electronic engineering information engineering business media_common Building automation |
| Zdroj: | BuildSys@SenSys |
| DOI: | 10.1145/2993422.2993426 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|