8.4 The Model Correspondence Problem

8.4 The Model Correspondence Problem

In the simple examples above, we have written Promela models by hand to verify concurrent execution in Java programs. One may ask how we can be sure that the Promela models accurately represent the possible behaviors of the Java programs, particularly if there are conceptual errors in the design of the Java programs. This is a serious problem, and it has no fully satisfactory solution.

We could verify correspondence between a finite state model and a program in one of three ways. First, we could automatically extract a model from the program source code (or compiled code, e.g., Java byte code), using procedures that we have verified once and for all. Second, we could turn the derivation relation around, producing program source code automatically from a model, treating the model as a kind of design document. The third option is to apply some combination of static analysis and testing to verify correspondence between model and program.

Automatically extracting models from programs is an attractive option, with the important advantage that the correctness of the extraction tool can be verified once and for all. In this approach, sophisticated and expensive verification can be justified and carried out by tool developers who are much more expert in finite state verification than users of the tool. The previous section strongly hints at the chief obstacle to model extraction: A model that blindly mirrors all details of program execution is likely to suffer from a much worse state space explosion than a model that has been carefully crafted to capture just the relevant essence of synchronization structure. A model that omits some crucial detail, on the other hand, can produce so many "false alarm" reports (failures that are possible in the model but not in the program) that the results are useless. The challenge for automatic model extraction, then, is to capture just enough of the relevant detail to be accurate, while abstracting enough to keep state space explosion under control.

Some abstraction of program details can be completely automated. For example, dependence analysis can be used to identify portions of the program that are irrelevant to checking a particular property. For this reason, it is often worthwhile to extract different models from the same program, to check different properties of interest. Where the required level of detail cannot be determined a priori by program analysis, sometimes a coarse initial model can be iteratively refined until either a verification or a counter-example is achieved. This is discussed further in Section 8.7.

Human cleverness in model design and automated support for model extraction are not mutually exclusive. For example, an important tactic in building finite state models is abstracting data values. It would be far too expensive to represent all the possible states of a queue of integers, for instance, but one might be able to capture enough information in the predicate isEmpty(Q). Sometimes a choice of predicates is strongly suggested by control structure of the program, and may even be found automatically by a model extraction tool. In other cases the user may be able to provide much better predicates to guide automated model extraction.

One can also reverse the model extraction process, starting with a finite state model and generating program code. Usually what can be generated is not the whole application, but it may be a component or skeleton in which the relevant behavior is localized. Essentially, this is equivalent to requiring the developer to manually distinguish the finite state model from other aspects of the application, but it can be much easier to specify how the finite state model is combined with other application details than to specify how the finite state model is extracted from the completed application. Program generation from (verifiable) finite state models, like program generation in general, is most applicable within constrained or well-understood application domains.

If a model is automatically extracted, or a program is automatically generated from a model, then correspondence between model and program can be verified once and for all by verifying the method of derivation. If, however, the derivation method is at least partly manual, then it will be necessary to gain confidence in their consistency by some other approach. Static program analysis can be helpful, but in the worst case a static analysis that verifies consistency between a model and a program can be as complex as a static analysis for extracting a model. More typically, conformance is verified by testing.

The details of an approach to conformance testing depend primarily on the form of the model and on what can be observed from program execution. A typical scenario is that the program model is equivalent to a deterministic finite state machine (FSM), and the only relevant observable aspect of program execution is a set of events (e.g., system calls or instrumented points) that correspond to event labels in the FSM model. A single execution is then consistent with the model if the observed sequence of execution events corresponds to a sequence of state transitions in a traversal of the model. The basic approach can be extended in several ways, for example, by testing against each of several communicating state machines separately or in parallel, by checking portions of program state against model state, or by considering multiple possible traversals in parallel if the model is inherently nondeterministic or the correspondence between observed program events and model state transitions is ambiguous. There is a welldeveloped body of testing techniques based on state machine models, some of which are discussed further in Chapter 14.

One may ask what advantage finite state verification has over simply testing the program for the property of interest, if we must still resort to conformance testing to verify the accuracy of a model. For example, if we are using finite state verification to show absence of race conditions, and then testing the program for conformance to the verified model, why not simply use testing to check for race conditions directly in the program?

In fact, the combination of finite state verification with testing can be both less expensive and more effective than testing alone. Consider again our simple example of misapplication of the double-check pattern in Figure 8.2. Tens of thousands of test executions can fail to reveal the race condition in this code, depending on the way threads are scheduled on a particular hardware platform and Java virtual machine implementation. Testing for a discrepancy between model and program, on the other hand, is fairly straightforward because the model of each individual state machine can be checked independently (in fact all but one are trivial). The complexity that stymies testing comes from nondeterministic interleaving of their execution, but this interleaving is completely irrelevant to conformance testing.