Parameterized Unit Testing with Pex, a White Box Test Input Generation Tool for .NET

Abstract

I will show how Parameterized Unit Tests (PUTs), a generalization of traditional unit tests, can be leveraged for systematic testing. PUTs are algebraic specifications written as code, describing the behavior of a program from a client's point of view. Traditional test cases can be obtained by supplying test inputs. Pex is a white box test input generation tool which analyzes the code of PUTs together with the program-under-test to determine relevant test inputs fully automatically. To this end, Pex performs dynamic symbolic execution, where the program is executed multiple times with different inputs while the taken execution paths are monitored. An SMT-solver with model-generation capabilities computes new test inputs that will exercise different execution paths. As a side effect of the analysis, Pex exposes bugs. The result is a traditional unit test suite with high code coverage. Pex has been used in Microsoft to test core .NET components. Pex is an incubation project for Visual Studio, and publicly available.

Short Bio

Nikolai Tillmann is a Principal Research Software Design Engineer at Microsoft Research. He is currently leading the Pex project. Previously he worked on AsmL, an executable modeling language, and Spec Explorer, a model-based testing tool. His research interests include program specification, analysis, testing, and verification. He received his M.S. (Diplom) in Computer Science from the Technical University of Berlin in 2000.

TecMF: TalkNikolai2009 (last edited 2010-08-11 15:16:52 by localhost)