TY - GEN
T1 - Randomized differential testing as a prelude to formal verification
AU - Groce, Alex
AU - Holzmann, Gerard
AU - Joshi, Rajeev
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=34548791741&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34548791741&partnerID=8YFLogxK
U2 - 10.1109/ICSE.2007.68
DO - 10.1109/ICSE.2007.68
M3 - Conference contribution
AN - SCOPUS:34548791741
SN - 0769528287
SN - 9780769528281
T3 - Proceedings - International Conference on Software Engineering
SP - 621
EP - 630
BT - Proceedings - 29th International Conference on Software Engineering, ICSE 2007
T2 - 29th International Conference on Software Engineering, ICSE 2007
Y2 - 20 May 2007 through 26 May 2007
ER -