Randomized Differential Testing as a Prelude to Formal Verification

TLDR

Flight software testing at JPL traditionally relies on hand‑crafted scenarios executed on hardware closely resembling mission systems. The study aims to integrate large‑scale biased randomized testing into flight software development on commodity desktop hardware. This integration is achieved by running large‑scale biased randomized tests on commodity desktop hardware. Using a reference implementation, fault‑injection hardware simulation, a testable design, and test minimization, the approach achieved high automation of fault detection and correction, showing that large‑scale randomized testing can accelerate on‑time delivery while preparing the way for subsequent heavyweight verification methods.

Abstract

Most flight software testing at the Jet Propulsion Laboratory relies on the use of hand-produced test scenarios and is executed on systems as similar as possible to actual mission hardware. We report on a flight software development effort incorporating large-scale (biased) randomized testing on commodity desktop hardware. The results show that use of a reference implementation, hardware simulation with fault injection, a testable design, and test minimization enabled a high degree of automation in fault detection and correction. Our experience will be of particular interest to developers working in domains where on-time delivery of software is critical (a strong argument for randomized automated testing) but not at the expense of correctness and reliability (a strong argument for model checking, theorem proving, and other heavyweight techniques). The effort spent in randomized testing can prepare the way for generating more complete confidence using heavyweight techniques.