Chapter 8: Finite State Verification

Finite state verification techniques are intermediate in power and cost between construction of simple control and data flow models, on the one hand, and reasoning with the full strength of symbolic execution and theorem proving on the other. They automatically explore finite but potentially very large representations of program behavior to address important properties. They are particularly useful for checking properties for which testing is inadequate. For example, synchronization faults in multi-threaded programs may trigger failures very rarely, or under conditions that are nearly impossible to re-create in testing, but finite state verification techniques can detect them by exhaustively considering all possible interleavings of concurrent processes. Finite state verification can similarly be used to systematically explore possible instantiations of a data model.

8.1 Overview

Most important properties of program execution are undecidable in general, but finite state verification can automatically prove some significant properties of a finite model of the infinite execution space. Of course, there is no magic: We must carefully reconcile and balance trade-offs among the generality of the properties to be checked, the class of programs or models that can be checked, computational effort, and human effort to use the techniques.

Symbolic execution and formal reasoning can prove many properties of program behavior, but the power to prove complex properties is obtained at the cost of devising complex conditions and invariants and expending potentially unbounded computational effort. Construction of control and data flow models, on the other hand, can be fully and efficiently automated, but is typically limited to very simple program properties. Finite state verification borrows techniques from symbolic execution and formal verification, but like control and data flow analysis, applies them to models that abstract the potentially infinite state space of program behavior into finite representations. Finite state verification techniques fall between basic flow analyses and full-blown formal verification in the richness of properties they can address and in the human guidance and computational effort they require.

Since even simple properties of programs are undecidable in general, one cannot expect an algorithmic technique to provide precise answers in all cases. Often finite state verification is used to augment or substitute for testing when the optimistic inaccuracy of testing (due to examining only a sample of the program state space) is unacceptable. Techniques are therefore often designed to provide results that are tantamount to formal proofs of program properties. In trade for this assurance, both the programs and properties that can be checked are severely restricted. Restrictions on program constructs typically appear in procedures for deriving a finite state model from a program, generating program code from a design model, or verifying consistency between a program and a separately constructed model.

Finite state verification techniques include algorithmic checks, but it is misleading to characterize them as completely automated. Human effort and considerable skill are usually required to prepare a finite state model and a suitable specification for the automated analysis step. Very often there is an iterative process in which the first several attempts at verification produce reports of impossible or unimportant faults, which are addressed by repeatedly refining the specification or the model.

The automated step can be computationally costly, and the computational cost can impact the cost of preparing the model and specification. A considerable amount of manual effort may be expended just in obtaining a model that can be analyzed within available time and memory, and tuning a model or specification to avoid combinatorial explosion is itself a demanding task. The manual task of refining a model and specification to obtain either assurance or useful reports of real faults in design or coding is much less expensive if the analysis step is near-interactive than if it requires several minutes or hours.

Some analysis techniques perform quite tolerably on small models, but their computational demands grow very rapidly with model size. These may be perfectly acceptable for a simple model of a critical component, such as a protocol whose description does not depend on the size of the system in which it is implemented. In other cases, scalability of the finite state verification technique is likely to be a limiting factor in its useful application.

Finite state verification techniques vary widely in the balance they strike on issues of generality, precision, automation, computational effort, and scalability. A core idea shared by all is that a question about a program is translated into a simpler question about a finite state model of the program, as illustrated in Figure 8.1. Ultimately, one question about the program (Does it conform to the property we want to check?) is divided into two (Does the model conform to the simpler property we can check? Is it an accurate model of the program?)

Figure 8.1: The finite state verification framework.

The model may be derived from an actual program, like the control flow and data flow models described in prior chapters, or from some other design artifact (e.g., a program specification). Restrictions on the program may be required to derive a model automatically from a program. It is also possible to derive program code from annotated models.^[1] If either the model or the program is derived automatically from the other, we may be able to do so in a way that guarantees consistency between the two.

We may also be able to check consistency automatically even if the derivation is not automatic. Alternatively, the accuracy of the model may be assessed by conformance testing, treating the model as a kind of specification. The combination of finite state verification and conformance testing is often more effective than directly testing for the property of interest, because a discrepancy that is easily discovered in conformance testing may very rarely lead to a run-time violation of the property (e.g., it is much easier to detect that a particular lock is not held during access to a shared data structure than to catch the occasional data race that the lock protects against).

A property to be checked can be implicit in a finite state verification tool (e.g., a tool specialized just for detecting potential null pointer references), or it may be expressed in a specification formalism that is purposely limited to a class of properties that can be effectively verified using a particular checking technique. Often the real property of interest is not amenable to efficient automated checking, but a simpler and more restrictive property is. That is, the property checked by a finite state verification tool may be sufficient but not necessary for the property of interest. For example, verifying freedom from race conditions on a shared data structure is much more difficult than verifying that some lock is always held by threads accessing that structure; the latter is a sufficient but not necessary condition for the former. This means that we may exclude correct software that we are not able to verify, but we can be sure that the accepted software satisfies the property of interest.

^[1]Note that one may independently derive several different models from one program, but deriving one program from several different models is much more difficult.