6.5 Related Work	131
set of documents and some loans still active	or with an empty
set of users and some loans still active	In fact, it is not possible

to remove a user who is borrowing some documents (see check performed at line 17), and it is not possible to remove a document that is borrowed by a user (see check performed at line 33). Consequently, when one or more loans are active (loans:some), the associated users and documents cannot be

removed from the library, thus making the states	and
unreachable.

6.5 Related Work

Recovering a finite state model of a program has been investigated in the context of model checking [15, 19]. One of the major obstacles that has been encountered in the extension of model checking from hardware to software verification is the problem of constructing a finite state model that approximates the executable behavior of a program in a reliable way. Manual construction of such models is expensive and error prone. For complex systems it is out of the question. The possibility of using abstract interpretation for this purpose has been investigated in [15, 19]. Automated support for the abstraction of the source code into a finite state model is provided by the tool Bandera, which allows for the integration of abstraction definitions into the source code of the program under analysis. Moreover, customization of the abstraction to check a particular property is also possible.

Another tool that employs abstraction to produce a tractable model of an input software system is Java Path Finder [95]. Program annotations consisting of user-defined predicates are used to generate another Java program in which concrete statements are replaced by the abstracted ones. Model checking is conducted on the abstracted version of the program, which exhibits a tractable, finite state, behavior. The model checker explores the state space by performing a symbolic execution of the program. The state being propagated in the symbolic execution includes a heap configuration, a path condition on primitive fields, and thread scheduling. Whenever the path condition is updated, it is checked for satisfiability using an external decision procedure. If it cannot be satisfied, the model checker backtracks. In this way, infeasible portions of the state space are not explored. Java Path Finder has been used for test case generation [96], with the test criterion (e.g., reaching every control flow branch) encoded as a property. When the model checker can determine a path along which such a property is true, associated with a satisfiable path condition, it is possible to find a witness, that is, a set of concrete values that make the path condition true and respect the constraints on the heap configuration (i.e., on the object fields referencing other objects). This is easily converted into a test case for the given program.

Besides program understanding, one of the most important applications of the state diagrams, possibly recovered from the code, is state-based testing [6,

132 6 State Diagrams

92]. According to this testing methodology, the class under test is modeled by its state diagram and a set of test cases is considered adequate for the unit test of the class when the states and the transitions in the state diagram are covered up to a level specified in the objective coverage criterion. The most widely used coverage criterion in state-based testing is transition coverage. It requires that all transitions from state to state be exercised at least once by some test case. This ensures that a class is not delivered with untested states or state transitions. As a support to defect finding, it forces programmers to test their code by exercising all the states and all the possible state changes triggered by messages received by the object under test.