Formal Methods for Test and Evaluation: Reasoning over Tests, Automated Test Synthesis, and System Diagnostics

Citation

Graebener, Josefine Berta Marie (2024) Formal Methods for Test and Evaluation: Reasoning over Tests, Automated Test Synthesis, and System Diagnostics. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/4xdc-b988. https://resolver.caltech.edu/CaltechTHESIS:05312024-094443866

Abstract

With the integration of autonomous systems into our everyday lives edging closer to reality, ensuring the safety of these systems is paramount. Part of the safety verification process is a rigorous testing procedure, which currently does not exist for autonomous vehicles. In this thesis, we aim to provide approaches using formal methods to increase the efficiency of testing campaigns. First, we provide a framework based on assume-guarantee contracts to specify tests in the form of a test structure. Using these test structures, we then show how to combine, split, and compare tests. Additionally, we characterize when tests can be combined and when the resulting test requires temporal constraints. Next, we demonstrate the approach on examples and find a strategy for a test agent using winning sets and Monte Carlo tree search.

Second, we present a framework to automatically synthesize a test environment, consisting of static and reactive obstacles, and dynamic test agents. We characterize the desired test behavior in a system and a test objective in the form of a linear temporal logic specification, consisting of sub-tasks commonly used for robotic missions. This test environment must ensure that the test is not impossible (i.e. a correct system can pass the test), but also that every test execution that satisfies the system objective also satisfies the test objective. We use tools from automata theory to construct the virtual product graph that represents all possible test executions, and the virtual system graph, which corresponds to the system's perspective. We formulate this routing problem as a network flow optimization on the virtual product graph in the form of a mixed integer linear program for different test environments. We show that this routing problem is NP-hard. We propose a counterexample-guided search using GR(1) synthesis to find a strategy for a test agent. This framework is demonstrated in several examples in simulation and hardware.

Lastly, we present a framework to diagnose a system-level fault by identifying the component responsible for the failure. We make use of assume-guarantee contracts and Pacti, a tool for compositional system analysis and design, to construct a diagnostics map, which allows us to trace a system-level guarantee to possible causes. We show that this framework can reduce the number of statements that need to be checked in the diagnostics process. We illustrate this framework on several abstract examples and two examples inspired by a real-world autonomous system.

Thesis Files