Abstractions for safety assurance of autonomous systems

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2023

Author dc:creator

• Hsieh, Chiao

Contributors dc:contributor

• Mitra, Sayan
• Parthasarathy, Madhusudan
• Misailovic, Sasa
• Bak, Stanley

• Autonomous Systems
• Safety Assurance
• Formal Verification
• Compositional Verification
• Distributed Robotics
• Learning-enabled Systems

Statement dc:rights

• Copyright 2023 Chiao Hsieh

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/120127

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F120127