{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T02:08:43Z","timestamp":1743041323259,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031377051"},{"type":"electronic","value":"9783031377068"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>AWS IoT Events is an AWS service that makes it easy to respond to events from IoT sensors and applications.<jats:italic>Detector models<\/jats:italic>in AWS IoT Events enable customers to monitor their equipment or device fleets for failures or changes in operation and trigger actions when such events occur. If these models are incorrect, they may become out-of-sync with the actual state of the equipment causing customers to be unable to respond to events occurring on it.<\/jats:p><jats:p>Working backwards from common mistakes made when creating detector models, we have created a set of automated analyzers that allow customers to prove their models are free from six common mistakes. Our analyzers have been running in the AWS IoT Events production service since December 2021. Our analyzers check six correctness properties in the production service in real time. 93% of customers of\u00a0AWS\u00a0IoT\u00a0Events\u00a0have run our analyzers without needing to have any knowledge of them. Our analyzers have reported property violations in 22% of submitted detector models in the production service.<\/jats:p>","DOI":"10.1007\/978-3-031-37706-8_2","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"27-39","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automated Analyses of\u00a0IOT Event Monitoring Systems"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Apicelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0909-8986","authenticated-orcid":false,"given":"Sam","family":"Bayless","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2459-1258","authenticated-orcid":false,"given":"Ankush","family":"Das","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0321-8155","authenticated-orcid":false,"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dhiva","family":"Jaganathan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saswat","family":"Padhi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9877-8926","authenticated-orcid":false,"given":"Vaibhav","family":"Sharma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3824-1435","authenticated-orcid":false,"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raveesh","family":"Yadav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-96142-2_3","volume-title":"Computer Aided Verification","author":"A Gacek","year":"2018","unstructured":"Gacek, A., Backes, J., Whalen, M., Wagner, L., Ghassabani, E.: The JKind model checker. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 20\u201327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_3"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Cho, C.Y., D\u2019Silva, V., Song, D.: Blitz: compositional bounded model checking for real-world programs. In: 2013 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 136\u2013146 (2013)","DOI":"10.1109\/ASE.2013.6693074"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-68167-2_14","volume-title":"Automated Technology for Verification and Analysis","author":"Z Baranov\u00e1","year":"2017","unstructured":"Baranov\u00e1, Z., et al.: Model checking of c and C++ with DIVINE 4. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 201\u2013207. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_14"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48166-4_10","volume-title":"Software Engineering","author":"A Gargantini","year":"1999","unstructured":"Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC\/SIGSOFT FSE -1999. LNCS, vol. 1687, pp. 146\u2013162. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48166-4_10"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Karamanolis, C., Giannakopoulou, D., Magee, J., Wheater, S.M.: Model checking of workflow schemas. In: Proceedings Fourth International Enterprise Distributed Objects Computing Conference, EDOC 2000, pp. 170\u2013179 (2000)","DOI":"10.1109\/EDOC.2000.882357"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-10575-8_1","volume-title":"Handbook of Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H.: Introduction to model checking. In: Handbook of Model Checking, pp. 1\u201326. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_1"},{"key":"2_CR7","unstructured":"Clarke Jr, E.M., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model checking. cyber physical systems series (2018)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: Incremental, inductive model checking. In: 2013 20th International Symposium on Temporal Representation and Reasoning, pp. 5\u20136 (2013)","DOI":"10.1109\/TIME.2013.9"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","volume-title":"Computer Aided Verification","author":"L de Moura","year":"2003","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Bounded model checking and induction: from refutation to verification. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 14\u201326. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_2"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Newcomb, J.L., Chandra, S., Jeannin, J.-B., Schlesinger, C., Sridharan, M.: IOTA: a calculus for internet of things automation. In: Proceedings of the 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, ser. Onward! 2017. New York, NY, USA, pp. 119\u2013133. Association for Computing Machinery (2017). https:\/\/doi.org\/10.1145\/3133850.3133860","DOI":"10.1145\/3133850.3133860"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Liang, C.-J. M., et al.: SIFT: building an internet of safe things. In: Proceedings of the 14th International Conference on Information Processing in Sensor Networks, ser. IPSN 2015. New York, NY, USA, pp. 298\u2013309. Association for Computing Machinery (2015). https:\/\/doi.org\/10.1145\/2737095.2737115","DOI":"10.1145\/2737095.2737115"},{"key":"2_CR12","unstructured":"Garc\u00eda-Herranz del Olmo, M., Haya, P.A., Alam\u00e1n, X.: Towards a ubiquitous end-user programming system for smart spaces. J. Univers. Comput. Sci. 16(12), 1633\u20131649 (2010)"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Ur, B., McManus, E., Pak Yong Ho, M., Littman, M.L.: Practical trigger-action programming in the smart home. In: Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, ser. CHI 2014. New York, NY, USA, pp. 803\u2013812. Association for Computing Machinery (2014). https:\/\/doi.org\/10.1145\/2556288.2557420","DOI":"10.1145\/2556288.2557420"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR15","unstructured":"Amazon Web Services, Inc., Find answers to AWS questions about AWS IoT Events, AWS (2021). https:\/\/repost.aws\/tags\/TANsxSwnClQ_Wfh-uklXi7hQ"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL 1982, New York, NY, USA, pp. 207\u2013212. Association for Computing Machinery (1982). https:\/\/doi.org\/10.1145\/582153.582176","DOI":"10.1145\/582153.582176"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348\u2013375 (1978). https:\/\/www.sciencedirect.com\/science\/article\/pii\/0022000078900144","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Hindley, R.: The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146, 29\u201360 (1969). http:\/\/www.jstor.org\/stable\/1995158","DOI":"10.2307\/1995158"},{"issue":"8","key":"2_CR19","doi-asserted-by":"publisher","first-page":"803","DOI":"10.1109\/TSE.2015.2421011","volume":"41","author":"G Gay","year":"2015","unstructured":"Gay, G., Staats, M., Whalen, M., Heimdahl, M.P.E.: The risks of coverage-directed test case generation. IEEE Trans. Softw. Eng. 41(8), 803\u2013819 (2015)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2_CR20","unstructured":"AWS IoT Events, Troubleshooting a detector model by running analyses (2021). https:\/\/docs.aws.amazon.com\/iotevents\/latest\/developerguide\/iotevents-analyze-api.html"},{"issue":"9","key":"2_CR21","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language LUSTRE. Proc. IEEE 79(9), 1305\u20131320 (1991)","journal-title":"Proc. IEEE"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37706-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T06:56:35Z","timestamp":1729752995000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37706-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377051","9783031377068"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37706-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}