Systematically Debugging IoT System Correctness for Home Automation
|Event Date:||April 21, 2017|
|Speaker Affiliation:||Associate Professor
Department of Computer Science and Technology Nanjing University, P.R. China
|Type:||Computer Engineering Research Area Seminar
|Contact Name:||Professor Xiaokang Qiu
|School or Program:||Electrical and Computer Engineering
Advances and standards in Internet of Things (IoT) have simplified the realization of home 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 talk 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.
Lei Bu is an associate professor in the Department of Computer Science and Technology, Nanjing University, P.R. China. He received his bachelor’s and PH.D. degrees in Computer Science from Nanjing University in 2004 and 2010. He was a visiting scholar at Carnegie Mellon University, Microsoft Research Asia, Fondazione Bruno Kessler, and University of Texas at Dallas.
His main research interests include formal methods, model checking, hybrid systems, and cyber-physical systems. He has published around 40 papers in leading journals and conferences including TC, RTSS, TPDS, STTT, DATE, VMCAI, CAV. He has been awarded Chinese computer federation young talent development program and Microsoft Research Asia Star Track young faculty program.