Case Studies in Software Model CheckingBlast is a
model checker for C programs: for a given property it computes a
counterexample, if the property was violated; or an approximation of
the complete state space, if the property holds; or it stops because of
time-out. We consider three practical applications of the model
checker to software engineering disciplines.
All three approaches are especially interesting for
quality assurance of the software system without manually changing the
program source code: the properties of the specification language are
specified separately from the source code, test data are fed through
the module interface, and memory safety is checked via fully automatic
instrumentation of the source code.
- We use the
counterexamples to generate test cases for statement and condition
coverage. The path-sensitive search in the abstract state space led to
a considerable reduction of the set of test cases.
use the specification language for Blast to define and verify
properties of C programs. The specification language supports two
abstraction: a monitor automaton describes path-oriented safety
properties, and a more abstract location-oriented query language allows
for combination of several path-oriented properties.
apply Blast to proving memory safety of C programs. For example, we
can prove if the program contains invalid pointer
dereferences. If such a situation is found, Blast reports a path
(counterexample) to the location in the program where the memory access
For each of the above applications of model checking in software engineering practice, we
provide one student project. The student project consists of applying
each of the above approaches to a case study, in order to find out for
which kind of C programs the method works conveniently.