{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/120127"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/120127","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Abstractions for safety assurance of autonomous systems","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-09-01 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-09-01 without embargo terms","abstract_has_math":false,"creators":["Hsieh, Chiao"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Mitra, Sayan","Parthasarathy, Madhusudan","Misailovic, Sasa","Bak, Stanley"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2023,"date_issued":"2023-05","date_published":"2023-05","updated_at":"2026-07-22T22:24:56Z","subjects":["Autonomous Systems","Safety Assurance","Formal Verification","Compositional Verification","Distributed Robotics","Learning-enabled Systems"],"languages":["en","eng"],"rights":["Copyright 2023 Chiao Hsieh"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/120127","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Mitra, Sayan","Parthasarathy, Madhusudan","Misailovic, Sasa","Bak, Stanley"]},{"key":"dc:creator","label":"Author","values":["Hsieh, Chiao"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2023-05","2023-04-28"]},{"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":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Autonomous Systems","Safety Assurance","Formal Verification","Compositional Verification","Distributed Robotics","Learning-enabled Systems"]}]},{"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 2023 Chiao Hsieh"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/120127"]}]},{"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 2023-09-01 without embargo terms","The student, Chiao Hsieh, accepted the attached license on 2023-04-28 at 09:30.","The student, Chiao Hsieh, submitted this Dissertation for approval on 2023-04-28 at 09:43.","This Dissertation was approved for publication on 2023-04-28 at 11:12.","DSpace SAF Submission Ingestion Package generated from Vireo submission #19215 on 2023-09-01 at 16:55:43","An autonomous system has components to perceive the environment, control the hardware, and communicate with other agents. Ideally, the formal analysis of the closed-loop system would have access to explicit models of all components. However, explicit models of perception and dynamics are often unavailable or intractable for formal verification. Instead, executable models for these components are available for simulation and testing in practice. In this thesis, we will present our compositional verification framework for certifying and assuring safety for systems with combinations of distributed communication, learning-enabled perception, and black-box dynamics. Our insight is to construct abstractions of these components for the end-to-end system-level safety analysis; then we empirically validate each component against its abstraction by sampling executable models. For distributed robotic applications, we focus on constructing the abstraction for heterogeneous motion dynamics. Our notion of port assumptions for dynamics decomposes the safety assurance into two steps: (a) the formal safety proof of the distributed system using port assumptions, and (b) the validation of port assumptions using data-driven reachability analyses. We learned that this compositional reasoning generalizes to both synchronous and asynchronous communications between heterogeneous vehicles. We are able to derive the collision avoidance guarantee in a distributed delivery application using our Koord framework for shared variable communication between ground vehicles and quadrotors. We apply the same idea on asynchronous message passing-based Unmanned Air-traffic Management protocols (UTM) and verify safe separations between quadrotors and fixed-wing airplanes. We also study autonomous systems with visual perception enabled by deep neural networks (DNNs). Our main insight is to search for ground truth-based approximate abstractions for perception. Our notion of approximate abstractions bypasses the challenges in the formal specification of perception and high dimensional image domains, and the precision of the approximate abstraction can be estimated empirically. We study both single agent and multiagent systems including three practical vision-based autonomous systems: (a) a lane tracking system for an autonomous vehicle, (b) a corn row following system for an agricultural robot, and (c) a vision-based multi-agent swarm formation. We are able to provide end-to-end assurance for all systems and examine the precision using simulations. In summary, our compositional verification framework outlines a pragmatic path to provide safety assurance of autonomous systems. We formalize (approximate) abstractions for compositional verification and develop approaches to search for abstractions. This allows us to formally verify as many components in the system as possible. For other components that are intractable for formal verification, we search for abstractions of these components and rigorously validate the abstractions via testing and data-driven verification. We are able to gain safety assurance using abstractions in all our case studies and validate the abstractions with high-fidelity Gazebo and AirSim simulations."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Abstractions for safety assurance of autonomous systems"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan","Parthasarathy, Madhusudan","Misailovic, Sasa","Bak, Stanley"],"dc:creator":["Hsieh, Chiao"],"dc:date":["2023-05","2023-04-28"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-09-01 without embargo terms","The student, Chiao Hsieh, accepted the attached license on 2023-04-28 at 09:30.","The student, Chiao Hsieh, submitted this Dissertation for approval on 2023-04-28 at 09:43.","This Dissertation was approved for publication on 2023-04-28 at 11:12.","DSpace SAF Submission Ingestion Package generated from Vireo submission #19215 on 2023-09-01 at 16:55:43","An autonomous system has components to perceive the environment, control the hardware, and communicate with other agents. Ideally, the formal analysis of the closed-loop system would have access to explicit models of all components. However, explicit models of perception and dynamics are often unavailable or intractable for formal verification. Instead, executable models for these components are available for simulation and testing in practice. In this thesis, we will present our compositional verification framework for certifying and assuring safety for systems with combinations of distributed communication, learning-enabled perception, and black-box dynamics. Our insight is to construct abstractions of these components for the end-to-end system-level safety analysis; then we empirically validate each component against its abstraction by sampling executable models. For distributed robotic applications, we focus on constructing the abstraction for heterogeneous motion dynamics. Our notion of port assumptions for dynamics decomposes the safety assurance into two steps: (a) the formal safety proof of the distributed system using port assumptions, and (b) the validation of port assumptions using data-driven reachability analyses. We learned that this compositional reasoning generalizes to both synchronous and asynchronous communications between heterogeneous vehicles. We are able to derive the collision avoidance guarantee in a distributed delivery application using our Koord framework for shared variable communication between ground vehicles and quadrotors. We apply the same idea on asynchronous message passing-based Unmanned Air-traffic Management protocols (UTM) and verify safe separations between quadrotors and fixed-wing airplanes. We also study autonomous systems with visual perception enabled by deep neural networks (DNNs). Our main insight is to search for ground truth-based approximate abstractions for perception. Our notion of approximate abstractions bypasses the challenges in the formal specification of perception and high dimensional image domains, and the precision of the approximate abstraction can be estimated empirically. We study both single agent and multiagent systems including three practical vision-based autonomous systems: (a) a lane tracking system for an autonomous vehicle, (b) a corn row following system for an agricultural robot, and (c) a vision-based multi-agent swarm formation. We are able to provide end-to-end assurance for all systems and examine the precision using simulations. In summary, our compositional verification framework outlines a pragmatic path to provide safety assurance of autonomous systems. We formalize (approximate) abstractions for compositional verification and develop approaches to search for abstractions. This allows us to formally verify as many components in the system as possible. For other components that are intractable for formal verification, we search for abstractions of these components and rigorously validate the abstractions via testing and data-driven verification. We are able to gain safety assurance using abstractions in all our case studies and validate the abstractions with high-fidelity Gazebo and AirSim simulations."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/120127"],"dc:language":["en","eng"],"dc:rights":["Copyright 2023 Chiao Hsieh"],"dc:subject":["Autonomous Systems","Safety Assurance","Formal Verification","Compositional Verification","Distributed Robotics","Learning-enabled Systems"],"dc:title":["Abstractions for safety assurance of autonomous systems"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:56Z"}