Systematically Ensuring the Confidence of Home Automation IoT Systems By Model Checking
Advances and standards in Internet of Things (IoT) have simplified the realization of home automation (HA). 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 MenShen framework which conducts the verification and debugging of HA-IoT system automatically. First, MenShen builds the formal model of the HA-IoT system automatically. Then, off-the-shelf model checkers can be utilized to check the correctness of the system. Last but not least, to debug the identified faults, MenShen selectively transforms the control system logics into a set of parameterized equations, which can then be solved by popular model checking tools to synthesize fix suggestions for non-expert users.
Mon 15 Jul (GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi change
|11:00 - 11:20|
|11:20 - 11:40|
|11:40 - 12:00|
|12:00 - 12:30|