University of Illinois Urbana-Champaign

Parallelization and incremental algorithms in the verse hybrid system verification library

Zhu, Haoqing

Content Files
ZHU-THESIS-2023.pdf

Permalink

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

Description

Title
Parallelization and incremental algorithms in the verse hybrid system verification library
Author(s)
Zhu, Haoqing
Issue Date
2023-05-04
Director of Research (if dissertation) or Advisor (if thesis)
Mitra, Sayan
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
M.S.
Degree Level
Thesis
Keyword(s)
  • Scenario verification
  • Reachability analysis
  • Hybrid Systems
  • Parallel programming
Abstract
Hybrid systems is a popular model for modeling and verifying cyber physical systems, combining the discrete transition logic and physical dynamics of agents. However, it is difficult for most users to adopt this technology without formal methods training. Verse is a verification library which tries to address this issue and make the hybrid system technology more usable. Verse has shown some promise and in a short amount of time is currently used by several research groups. But Verse has scalability issues yet to be solved. In this thesis, we present parallelization and incremental verification algorithms in Verse. Verse computes reachsets of a system as a reachability tree, and the parallelization algorithm can compute different parts of the tree concurrently in different processors. Using the popular Ray parallelization framework, we are able to efficiently parallelize the computations without the use of locks. The incremental verification algorithm can reuse computation from previous experiments and reduce computation time for similar scenarios. We evaluate the implementation of our algorithms on a variety of scenarios, and observed that we can achieve 2 to 4 times speedup on moderately large scenarios. In one experiment with 12 agents and 133 transitions, we are able to compute the reachsets in 8 minutes 30 seconds, a 3.5x speedup over the previous 30 minutes.
Graduation Semester
2023-05
Type of Resource
Thesis
Handle URL
https://hdl.handle.net/2142/120171
Copyright and License Information
Copyright 2023 Haoqing Zhu

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois