Abstract
Testing is the dominating verification technique used in industry today, and many man-hours and resources are invested in the testing of software prod- ucts. To cut down the cost of testing, automated test execution becomes more and more popular. However, the selection of which tests to be exe- cuted is still mainly a manual process that is error prone, and often without sufficient guarantees that the system will be systematically tested. A way to achieve systematic testing is to ensure that the tests satisfy a required coverage criterion.

In this thesis two main problems are addressed: the problem of how to formally specify coverage criteria, and the problem of how to generate a test suite from a formal system model, such that the test suite satisfies a given coverage criterion. We also address the problem of how to generate an optimal test suite, e.g., with respect to the total time required to execute the test suite.

Our approach is to convert the test case generation problem into a reach- ability problem. We observe that a coverage criterion consists of a set of items, which we call coverage items. The problem of generating a test case for each coverage item can be treated as separate reachability problems. We use an on-the-fly method, where coverage information is added to the states of the analyzed system model, to solve the reachability problem of a cover- age item. The coverage information is used to select a set of test cases that together satisfy all the coverage items, and thus the full coverage criterion.

Based on the view of coverage items we define a language, in the form of parameterized observer automata, to formally describe coverage criteria. We show that the language is expressive enough to describe a variety of common coverage criteria in the literature. Two different ways to generate test suites form a system model and a given coverage criterion are presented. The first way is based on model annotations and uses the model checker Uppaal. The second way, where no annotations are needed, is a modified reachability analysis algorithm that is implemented in an extended version of the Uppaal tool.

The full thesis is available at http://user.it.uu.se/~hessel/lic/AHLic.pdf

Opponent: Dr Henrik Thane, Mälardalen University, Sweden.

ASTEC seminar

Place: 1311, Department of Information Technology , Uppsala university
Time: 13.15, March 7, 2006