Randomized differential testing as a prelude to formal verification

Alex Groce, Gerard Holzmann, Rajeev Joshi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

86 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProceedings - 29th International Conference on Software Engineering, ICSE 2007
Pages621-630
Number of pages10
DOIs
StatePublished - 2007
Externally publishedYes
Event29th International Conference on Software Engineering, ICSE 2007 - Minneapolis, MN, United States
Duration: May 20 2007May 26 2007

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257

Other

Other29th International Conference on Software Engineering, ICSE 2007
Country/TerritoryUnited States
CityMinneapolis, MN
Period5/20/075/26/07

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Randomized differential testing as a prelude to formal verification'. Together they form a unique fingerprint.

Cite this