Abstractions for safety assurance of autonomous systems

Hsieh, Chiao

Permalink

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

Description

Title

Abstractions for safety assurance of autonomous systems

Author(s)

Hsieh, Chiao

Issue Date

2023-04-28

Director of Research (if dissertation) or Advisor (if thesis)

Mitra, Sayan

Doctoral Committee Chair(s)

Mitra, Sayan

Committee Member(s)

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

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• autonomous systems
• safety assurance
• formal verification
• compositional verification
• distributed robotics
• learning-enabled systems

Abstract

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.

Graduation Semester

2023-05

Type of Resource

Thesis

Copyright and License Information

Copyright 2023 Chiao Hsieh

Owning Collections