A commonly used dictum in software testing indicates that “the only exhaustive means of testing is testing until the tester is exhausted!” Not so, say the authors of this paper, if your software is implementing a model representing some logic that lends itself to formal mathematical verification.

Miller, Whalen, and Cofer present a translator framework to enable the use of model checkers to determine if a model satisfies a given set of properties. A model checker is created to consider all possible combinations of inputs and state, thus enabling exhaustive testing of the model. After a small example, the authors present an overview of three case studies in which they have applied their tools for model checking. The first one deals with a commercial aircraft’s adaptive display and guidance system window manager. The other two deal with the operational flight program of an unmanned aerial vehicle. The case studies conclude that model checking can be effectively used to discover errors early in the development life cycle, for many classes of models.

This is an interesting paper. I recommend it to software testing researchers, practitioners, and managers.