Software tools for scenario verification of autonomous systems exploiting dynamical symmetries

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.U of I OnlyAuthor requested U of Illinois access only (OA after 2yrs) in Vireo ETD syste