{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/129213"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/129213","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Efficient static checking of safety properties in concurrent smart environments","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","abstract_has_math":false,"creators":["Menezes, Rishabh"],"institution":"University of Illinois Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Gupta, Indranil"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2025,"date_issued":"2025-04-18","date_published":"2025-04-18","updated_at":"2026-07-22T22:25:04Z","subjects":["Distributed Systems","Internet-of-Things","Safety Properties","Concurrent Systems","Formal Modeling","Model Checking","Smart Homes"],"languages":["en","eng"],"rights":["Copyright 2025 Rishabh Menezes"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/129213","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Gupta, Indranil"]},{"key":"dc:creator","label":"Author","values":["Menezes, Rishabh"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2025-04-18","2025-05"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Distributed Systems","Internet-of-Things","Safety Properties","Concurrent Systems","Formal Modeling","Model Checking","Smart Homes"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2025 Rishabh Menezes"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/129213"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","The student, Rishabh Menezes, accepted the attached license on 2025-04-17 at 00:02.","The student, Rishabh Menezes, submitted this Thesis for approval on 2025-04-17 at 22:12.","This Thesis was approved for publication on 2025-04-18 at 10:54.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21811 on 2025-10-19 at 18:09:30","The Internet of Things (IoT) space in smart environments, including homes and buildings, presents key challenges in the realm of automation safety. Users can control smart devices with routines, or command sequences that operate serially individually but out of order with respect to each other. While this concurrency can be useful for parallelizing tasks, it can also make the smart environment susceptible to entering undesirable or unpredictable states. As smart device effects have real-world consequences for end users and their property, preventing aberrant executions is of critical importance. This thesis presents verification methods for the static version of this problem, where safety is checked at routine submission time. It will contribute (i) a method of safety specification, by which users can express safety conditions to be held as invariants, and (ii) solutions for static checking of routines against specified safety conditions. As the latter problem is NP-hard, the thesis first presents a system of algorithms that demonstrate model-specific optimizations which improve runtime performance through a conservative approach to safety, provably catching 100% of safety violations. The thesis secondly contributes a generic formal model of the smart environment in a popular specification and verification language called Maude, which enables users to model check a given configuration of devices and routines against safety conditions to find any violations."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Efficient static checking of safety properties in concurrent smart environments"]}]}],"canonical_facts":{"dc:contributor":["Gupta, Indranil"],"dc:creator":["Menezes, Rishabh"],"dc:date":["2025-04-18","2025-05"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","The student, Rishabh Menezes, accepted the attached license on 2025-04-17 at 00:02.","The student, Rishabh Menezes, submitted this Thesis for approval on 2025-04-17 at 22:12.","This Thesis was approved for publication on 2025-04-18 at 10:54.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21811 on 2025-10-19 at 18:09:30","The Internet of Things (IoT) space in smart environments, including homes and buildings, presents key challenges in the realm of automation safety. Users can control smart devices with routines, or command sequences that operate serially individually but out of order with respect to each other. While this concurrency can be useful for parallelizing tasks, it can also make the smart environment susceptible to entering undesirable or unpredictable states. As smart device effects have real-world consequences for end users and their property, preventing aberrant executions is of critical importance. This thesis presents verification methods for the static version of this problem, where safety is checked at routine submission time. It will contribute (i) a method of safety specification, by which users can express safety conditions to be held as invariants, and (ii) solutions for static checking of routines against specified safety conditions. As the latter problem is NP-hard, the thesis first presents a system of algorithms that demonstrate model-specific optimizations which improve runtime performance through a conservative approach to safety, provably catching 100% of safety violations. The thesis secondly contributes a generic formal model of the smart environment in a popular specification and verification language called Maude, which enables users to model check a given configuration of devices and routines against safety conditions to find any violations."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/129213"],"dc:language":["en","eng"],"dc:rights":["Copyright 2025 Rishabh Menezes"],"dc:subject":["Distributed Systems","Internet-of-Things","Safety Properties","Concurrent Systems","Formal Modeling","Model Checking","Smart Homes"],"dc:title":["Efficient static checking of safety properties in concurrent smart environments"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:04Z"}