Implicit Invariants for Relational Data Structures



Robotics utilizes algorithms for control, localization, and navigation that rely heavily on complex data structures such as matrices and graphs. The values of these data structures are the result of interleaved controllers and complex interactions between equations that are difficult to parameterize as they relate to observed behavior. This makes the maintenance of these data structures both diffi- cult to track and highly critical to the successful operation of the system. Therefore, there is a demonstrable need to generate new types of invariants to better characterize the connection between control behavior and robustness. This work builds and generates novel invariants to cap- ture the behavior of these complex data structures in both instantaneous and time-bounded contexts. Then, this in- variant generation is applied to a testbed of simulated CPS deployments. Capturing these invariants will enable the discovery of relations between member variables and model how data structures change over time.

Recommended citation: Meriel von Stein. Implicit Invariants for Relational Data Structures. MS Thesis, University of Virginia, 2020.

Download: [Presentation] [Paper]