Graebener, Josefine B. and Badithela, Apurva and Murray, Richard M. (2022) Towards Better Test Coverage: Merging Unit Tests for Autonomous Systems. In: NASA Formal Methods: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings. Lecture Notes in Computer Science. No.13260. Springer , Cham, pp. 133-155. ISBN 9783031067723. https://resolver.caltech.edu/CaltechAUTHORS:20220715-744315000
![]() |
PDF
- Accepted Version
Creative Commons Attribution Non-commercial Share Alike. 1MB |
Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:20220715-744315000
Abstract
We present a framework for merging unit tests for autonomous systems. Typically, it is intractable to test an autonomous system for every scenario in its operating environment. The question of whether it is possible to design a single test for multiple requirements of the system motivates this work. First, we formally define three attributes of a test: a test specification that characterizes behaviors observed in a test execution, a test environment, and a test policy. Using the merge operator from contract-based design theory, we provide a formalism to construct a merged test specification from two unit test specifications. Temporal constraints on the merged test specification guarantee that non-trivial satisfaction of both unit test specifications is necessary for a successful merged test execution. We assume that the test environment remains the same across the unit tests and the merged test. Given a test specification and a test environment, we synthesize a test policy filter using a receding horizon approach, and use the test policy filter to guide a search procedure (e.g. Monte-Carlo Tree Search) to find a test policy that is guaranteed to satisfy the test specification. This search procedure finds a test policy that maximizes a pre-defined robustness metric for the test while the filter guarantees a test policy for satisfying the test specification. We prove that our algorithm is sound. Furthermore, the receding horizon approach to synthesizing the filter ensures that our algorithm is scalable. Finally, we show that merging unit tests is impactful for designing efficient test campaigns to achieve similar levels of coverage in fewer test executions. We illustrate our framework on two self-driving examples in a discrete-state setting.
Item Type: | Book Section | |||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Related URLs: |
| |||||||||||||||
ORCID: |
| |||||||||||||||
Additional Information: | © 2022 Springer Nature Switzerland AG. J. B. Graebener and A. Badithela—Contributed equally to this work. We thank Dr. Ioannis Filippidis, Dr. Tichakorn Wongpiromsarn, Íñigo Íncer Romeo, Dr. Qiming Zhao, Dr. Michel Ingham, and Dr. Karena Cai for valuable discussions that helped shape this work. The authors acknowledge funding from AFOSR Test and Evaluation program, grant FA9550-19-1-0302 and National Science Foundation award CNS-1932091. | |||||||||||||||
Funders: |
| |||||||||||||||
Subject Keywords: | Testing of autonomous systems · Assume-guarantee contracts · Receding horizon synthesis | |||||||||||||||
Series Name: | Lecture Notes in Computer Science | |||||||||||||||
Issue or Number: | 13260 | |||||||||||||||
DOI: | 10.1007/978-3-031-06773-0_7 | |||||||||||||||
Record Number: | CaltechAUTHORS:20220715-744315000 | |||||||||||||||
Persistent URL: | https://resolver.caltech.edu/CaltechAUTHORS:20220715-744315000 | |||||||||||||||
Usage Policy: | No commercial reproduction, distribution, display or performance rights in this work are provided. | |||||||||||||||
ID Code: | 115651 | |||||||||||||||
Collection: | CaltechAUTHORS | |||||||||||||||
Deposited By: | George Porter | |||||||||||||||
Deposited On: | 22 Jul 2022 20:17 | |||||||||||||||
Last Modified: | 22 Jul 2022 20:17 |
Repository Staff Only: item control page