{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T23:16:03Z","timestamp":1780442163347,"version":"3.54.1"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2018,6,13]],"date-time":"2018-06-13T00:00:00Z","timestamp":1528848000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS 1553273 and CNS 1463722"],"award-info":[{"award-number":["CNS 1553273 and CNS 1463722"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61690204, 61632015, 61561146394, 61572249 and 61472179"],"award-info":[{"award-number":["61690204, 61632015, 61561146394, 61572249 and 61472179"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Microsoft Research Asia Collaborative Research Program"},{"name":"NSFC-ISF Research Program","award":["61561146394"],"award-info":[{"award-number":["61561146394"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2018,7,31]]},"abstract":"<jats:p>Recent advances and industry standards in Internet of Things (IoT) have accelerated the real-world adoption of connected devices. To manage this hybrid system of digital real-time devices and analog environments, the industry has pushed several popular home automation IoT (HA-IoT) frameworks, such as If-This-Then-That (IFTTT), Apple HomeKit, and Google Brillo. Typically, users author device interactions by specifying the triggering sensor event and the triggered device command. In this seemingly simple software system, two dominant factors govern the system confidence properties with respect to the physical world. First, IoT users are largely nonexperts who lack the comprehensive consideration regarding potential impact and joint effect with existing rules. Second, while the increasing complexity of IoT devices enables fine-grained control (e.g., heater temperature) of continuous real-time environments, even two simply connected devices can have a huge state space to explore. In fact, bugs that wrongfully control devices and home appliances can have ramifications on system correctness and even user physical safety. It is crucial to help users to make sure the system they created meets their expectation. In this article we introduce how techniques from hybrid automata can be practically applied to assist nonexpert IoT users in the confidence checking of such hybrid HA-IoT systems. We propose an automated framework for end-to-end programming assistance. We build and check the Linear Hybrid Automata (LHA) model of the system automatically. We also present a quantifier elimination-based method to analyze the counterexample found and synthesize fix suggestions. We implemented a platform, MenShen, based on this framework and proposed techniques. We conducted sets of real HA-IoT case studies with up to 46 devices and 65 rules. Empirical results show that MenShen can find violations and generate rule fix suggestions in only 10 seconds.<\/jats:p>","DOI":"10.1145\/3185501","type":"journal-article","created":{"date-parts":[[2018,6,15]],"date-time":"2018-06-15T14:18:30Z","timestamp":1529072310000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Systematically Ensuring the Confidence of Real-Time Home Automation IoT Systems"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0517-7801","authenticated-orcid":false,"given":"Lei","family":"Bu","sequence":"first","affiliation":[{"name":"Nanjing University, Jiangsu, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wen","family":"Xiong","sequence":"additional","affiliation":[{"name":"Nanjing University, Jiangsu, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chieh-Jan Mike","family":"Liang","sequence":"additional","affiliation":[{"name":"Microsoft Research, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shi","family":"Han","sequence":"additional","affiliation":[{"name":"Microsoft Research, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dongmei","family":"Zhang","sequence":"additional","affiliation":[{"name":"Microsoft Research, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shan","family":"Lin","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, NY"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[{"name":"Nanjing University, Jiangsu, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,6,13]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Apple HomeKit. 2016. Apple HomeKit. Retrieved from http:\/\/www.apple.com\/ios\/homekit\/.  Apple HomeKit. 2016. Apple HomeKit. Retrieved from http:\/\/www.apple.com\/ios\/homekit\/."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.12.022"},{"key":"e_1_2_1_3_1","unstructured":"AWS IoT. 2015. Device Registry for AWS IoT. Retrieved from http:\/\/docs.aws.amazon.com\/iot\/latest\/developerguide\/thing-registry.html.  AWS IoT. 2015. Device Registry for AWS IoT. Retrieved from http:\/\/docs.aws.amazon.com\/iot\/latest\/developerguide\/thing-registry.html."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946291"},{"key":"e_1_2_1_6_1","unstructured":"Lei Bu. 2006. BACH. Retrieved from http:\/\/seg.nju.edu.cn\/BACH\/.  Lei Bu. 2006. BACH. Retrieved from http:\/\/seg.nju.edu.cn\/BACH\/."},{"key":"e_1_2_1_7_1","unstructured":"Lei Bu. 2016. MenShen Project Page. Retrieved from http:\/\/seg.nju.edu.cn\/MenShen\/.  Lei Bu. 2016. MenShen Project Page. Retrieved from http:\/\/seg.nju.edu.cn\/MenShen\/."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0163-9"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517433"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000367.2000368"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679406"},{"key":"e_1_2_1_12_1","volume-title":"Peled","author":"Clarke Edmund","year":"2001"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the National Workshop for Research on High-Confidence Transportation Cyber-Physical Systems: Automotive, Aviation and Rail.","author":"Clarke Edmund","year":"2008"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2813767.2813780"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_16_1","unstructured":"Andreas Dolzmann. 2006. Redlog. Retrieved from http:\/\/redlog.eu\/.  Andreas Dolzmann. 2006. Redlog. Retrieved from http:\/\/redlog.eu\/."},{"key":"e_1_2_1_17_1","unstructured":"Google Brillo. 2016. Google Brillo. Retrieved from https:\/\/developers.google.com\/brillo\/.  Google Brillo. 2016. Google Brillo. Retrieved from https:\/\/developers.google.com\/brillo\/."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78929-1_14"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509434"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788803"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_2_1_22_1","volume-title":"Henzinger and Howard Wong-Toi","author":"Thomas","year":"1995"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1278460.1278462"},{"key":"e_1_2_1_24_1","volume-title":"IFTTT: Put the internet to work for you.","author":"IFTTT.","year":"2011"},{"key":"e_1_2_1_25_1","unstructured":"Json.NET. 2009. Json.Net. Retrieved from https:\/\/www.newtonsoft.com\/json.  Json.NET. 2009. Json.Net. Retrieved from https:\/\/www.newtonsoft.com\/json."},{"key":"e_1_2_1_26_1","volume-title":"Cyber- physical systems- are computing foundations adequate?Position Paper for NSF Workshop on Cyber-Physical Systems: Research Motivation, Techniques and Roadmap","author":"Lee Edward"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.023"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993422.2993426"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737095.2737115"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1366283.1366305"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_18"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2014.6843717"},{"key":"e_1_2_1_33_1","volume-title":"Response Times: The 3 Important Limits.","author":"Nielsen Norman Group","year":"1993"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25141-7_2"},{"key":"e_1_2_1_35_1","unstructured":"Universal Devices Products. 2007. Universaldevicesproducts\/insteon\/isy-99iseries. Retrieved from http:\/\/www.universal-devices.com\/.  Universal Devices Products. 2007. Universaldevicesproducts\/insteon\/isy-99iseries. Retrieved from http:\/\/www.universal-devices.com\/."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0210-3"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3185501","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3185501","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3185501","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:26:36Z","timestamp":1750213596000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3185501"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,13]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,7,31]]}},"alternative-id":["10.1145\/3185501"],"URL":"https:\/\/doi.org\/10.1145\/3185501","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,6,13]]},"assertion":[{"value":"2016-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-06-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}