Query-Driven Program Testing

摘要

We present a new approach to program testing which enables the pro-grammer to specify test suites in terms of a versatile query language. Our querylanguage subsumes standard coverage criteria ranging from simple basic blockcoverage all the way to predicate complete coverage and multiple condition cov-erage, but also facilitates on-the-fly requests for test suites specific to the codestructure, to external requirements, or to ad hoc needs arising in program un-derstanding/exploration. The query language is supported by a model checkingbackend which employs the CBMC framework. Our main algorithmic contribu-tion is a method called iterative constraint strengthening which enables us tosolve a query for an arbitrary coverage criterion by a single call to the modelchecker and a novel form of incremental SAT solving: Whenever the SAT solverfinds a solution, our algorithm compares this solution against the coverage crite-rion, and strengthens the clause database with additional clauses which excluderedundant new solutions. We demonstrate the scalability of our approach and itsability to compute compact test suites with experiments involving device drivers,automotive controllers, and open source projects.