Practical Formal Verification: How Close are We?

by
Professor Amir Pnueli
Weizmann Institute of Science, Israel

It is time that formal verification (of both software and hardware systems) be promoted from an art practiced by the enlightened few to an activity routinely and mundanely performed by a cadre of Verification Engineers (a new profession), as a standard part of the system development process.

In the talk, we will assess how far we are from the realization of this goal.

The talk focuses on the verification of Reactive Systems, specified by Temporal Logic. Reactive systems are ones whose role is to maintain an ongoing interaction with their environment, rather than produce a final result upon termination. Most embedded systems which control an external physical environment belong to this important class. Such systems must be specified and analyzed in terms of their BEHAVIORS.

Temporal Logic (TL) is introduced as a language for writing predicates over sequences of states (equivalently actions), thus specifying a subset of all possible behaviors as being ''acceptable'', and providing an abstract specification of a reactive systems. We discuss two prevalent styles of reactive specification: The Requirement List style, and the Reference Model style. It is shown that TL is adequate for both specification styles.

Two approaches are presented for verifying that a given Reactive System satisfies a temporal specification: the Deductive and the Explorative approaches. The deductive approach employs deductive rules and auxiliary constructs provided by the user, to reduce the temporal verification problem into a set of first-order implications that can be proven by available theorem-proving systems, such as PVS, SteP, or HOL.

The explorative approach (also termed model-checking, e.g., SMV, Formal Check) is based on a traversal of a graph consisting of all the reachable states of the given system, and checking which states satisfy each sub-formula of the specification. The development of the method of Symbolic Model Checking transformed the explorative approach into the method most widely used in industry. The main advantage of the explorative approach is that it is algorithmic and requires no user intervention. The main disadvantage is that it is restricted to finite-state systems.

With this background, we will analyze the distance to our ultimate goal in terms of:

1. The current state of the art of existing verification approaches and tools of the two prevalent kinds: Model Checking and Deductive Verification. The power, accessibility, friendliness, ease of use and operation of existing tools, and the size of systems they can verify. The qualification and sophistication required of a potential user.
2. The degree of acceptability and future expectations of formal verification within different industrial sectors.
3. The educational background and a proposed curriculum for the new discipline of Verification Engineering.
4. Integration of formal verification with other commonly practiced methods of validation such as testing and simulation.
5. The main obstacles standing in the way: the needs for user interaction. We will analyze the various places where user creativity is called for, such as in the design of powerful abstractions, reduction by symmetry and similarity, and the construction of auxiliary invariants and progress measures. It will be shown that, for particular classes of applications, it is possible to identify verification patterns and application-specific heuristics that can significantly reduce the amount of fresh intellectual effort needed for the consideration of each new instance of a system in this class.

In the last part of the talk, we will sketch recent progress in the extension of the formal-verification technologies to deal with real-time systems and hybrid systems.