A Caltech Library Service

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


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.


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.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:test and evaluation, contract-based design
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Aerospace Engineering
Minor Option:Computer Science
Awards:Ernest E. Sechler Memorial Award in Aeronautics, 2022.
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Murray, Richard M.
Thesis Committee:
  • Meiron, Daniel I. (chair)
  • Burdick, Joel Wakeman
  • Chung, Soon-Jo
  • Murray, Richard M.
Defense Date:30 April 2024
Funding AgencyGrant Number
Air Force Office of Scientific Research (AFOSR)FA9550-22-1-0333
Air Force Office of Scientific Research (AFOSR)FA9550-19-1-0302
Record Number:CaltechTHESIS:05312024-094443866
Persistent URL:
Related URLs:
URLURL TypeDescription adapted for Ch. 4 adapted for Ch. 3 work for Ch. 4 incorporated and adapted in Ch. 3
Graebener, Josefine Berta Marie0000-0002-1376-0741
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:16453
Deposited By: Josefine Graebener
Deposited On:31 May 2024 23:49
Last Modified:17 Jun 2024 19:53

Thesis Files

[img] PDF - Final Version
See Usage Policy.


Repository Staff Only: item control page