Accelerating cerification of cyber-physical systems using symmetry

Autonomous systems are increasingly being deployed in safety-critical applications such as transportation and medicine. Numerous approaches to analyze their safety have been considered including testing, falsification, and formal verification. The major challenge for all of these approaches is scalability to large and complex models. To address this challenge, we propose to use the symmetry naturally present in the dynamics of many of these systems. Reachability-based safety analysis simulates the dynamical models of the autonomous systems, such as differential equations or hybrid automata, and checks if any of their reachable states is unsafe. Symmetries in dynamical systems are maps that transform any of their trajectories to other trajectories. In this thesis, we show how to use known symmetries of autonomous systems to cache their reachable states and abstract their dynamical models to accelerate their safety analysis. The main contributions of this thesis are as follows: 1. Augmenting a state-of-the-art data-driven safety verification algorithm with a cache to reuse computed sets of reachable states. The proposed algorithm uses symmetries of the model under verification to increase the cache hit rate. 2. Augmenting traditional hybrid automata safety verification algorithms with a cache to reuse computed sets of reachable states. The proposed algorithm uses symmetries to share computed reachable sets between different modes and automata being verified. 3. Abstracting hybrid automata by combining modes with symmetric dynamics in the same abstract modes. 4. Designing a symmetry-based counter-example guided abstraction-refinement (CEGAR) algorithm for hybrid automata with symmetric continuous dynamics to accelerate their safety verification. 5. Finally, designing an efficient testing algorithm for autonomous systems that uses a cache to share symmetric trajectories among the test cases of a test suite, avoiding repetition of high-fidelity simulations. The algorithmic contributions of this thesis come with theoretical guarantees that ensure their soundness and completeness. The algorithms presented build on top of state-of-the-art reachability analysis and verification algorithms. They accelerate their computations, without affecting their soundness and completeness guarantees. Finally, we present software implementations and empirical analyses of the different algorithms presented, showing up to orders of magnitude speedup in verification and testing time of different dynamical models including a car, fixed-wing aircraft, a neural network-controlled quadrotor, and a Gazebo-based Hector quadrotor.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Electrical & Computer Engr

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2022

Author dc:creator

• Sibai, Hussein

Contributors dc:contributor

• Mitra, Sayan
• Liberzon, Daniel
• Forsyth, David
• Dullerud, Geir
• Misailovic, Sasa

• Engineering

Statement dc:rights

• Copyright 2021 Hussein Sibai

Language dc:language

en, eng

Handle dc:identifier

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

OAI record oai:identifier

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