Software tools for scenario verification of autonomous systems exploiting dynamical symmetries

Li, Yangge

Permalink

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

Description

Title

Software tools for scenario verification of autonomous systems exploiting dynamical symmetries

Author(s)

Li, Yangge

Issue Date

2021-12-06

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

Mitra, Sayan

Department of Study

Electrical & Computer Eng

Discipline

Electrical & Computer Engr

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

M.S.

Degree Level

Thesis

Keyword(s)

• Hybrid systems
• Multi-agent system
• Safety verification
• Online verification
• Symmetry
• Cloud computing

Abstract

In this thesis, we discuss using formal verification techniques to ensure the safety of autonomous systems. We present a particular type of verification problem called scenario verification, which involves vehicles executing complex plans in large cluttered workspaces. To solve the scenario verification problem, we present the tool SceneChecker. SceneChecker converts the scenario verification problem to a standard hybrid system verification problem and solves it effectively by exploiting structural properties in the plan and the vehicle dynamics. SceneChecker implements symmetry abstractions, a novel refinement algorithm, and is built to enhance the performance of existing reachability analysis tools as a plug-in subroutine. We evaluated SceneChecker on several complicated scenarios with different types of agents. Compared to two leading tools, DryVR and Flow*, SceneChecker shows 20x speedup in verification time, even while using those tools as reachability subroutines. We further look into a variation of the scenario verification problem, with multiple agents running independently in the shared workspace. In addition, the plan is generated as the agent executing the scenario, which requires safety checking to be performed during runtime. To solve this problem, we present Swerve, an open-source cloud computing toolkit for efficient runtime collision checking for multi-agent autonomous systems. Swerve implements a remote server to check safety for different agents by using boundedtime reachability analysis. In addition, Swerve implements a cache to store already computed reachable sets and reuses them to avoid repeated computations. We evaluate Swerve on several scenarios and are able to show that Swerve is able to properly detect potential collisions between agents and static obstacles. In addition, we show that with symmetry and caching, Swerve is able to obtain 16x average speedup in service response time.

Graduation Semester

2021-12

Type of Resource

Thesis

Permalink

http://hdl.handle.net/2142/114011

Copyright and License Information

Copyright 2021 Yangge Li

Owning Collections