Echo: Practical Formal Verification by Reverse Synthesis

Safe operation is crucial to safety-critical systems, such as fly-by-wire flight-control systems in aircraft. Software in these systems has to be correct, or, more precisely, the risk of being incorrect has to be reduced to an acceptable level. Ensuring the absence of implementation flaws by testing only is inadequate because it is infeasible to conduct the number of test cases required to establish a very high level of confidence. Thus formal specification and formally verified implementation are desirable.

Current approaches to formal verification are powerful but not sufficiently practical. Verification techniques are difficult and time-consuming to apply, tools are of limited capabilities and cannot be integrated, and the process requires high levels of expertise. Current approaches also impose limitations on developers that make it difficult to fit formal verification into the existing development cycle.

To address these problems, I develop a practical and effective approach to formal verification of the functional correctness of computer software. My approach, named Echo, relies upon and incorporates a number of powerful existing notations, tools and techniques, and distributes the verification burden over separate levels. At the core of the approach is a process called reverse synthesis in which a high-level abstract specification is extracted from the source code coupled with a low-level, detailed specification of a software system. Formal verification then involves two proofs each of which is either generated automatically or mechanically checked. These proofs are: (1) a proof that the software source code implements the low-level specification correctly; and (2) a proof that the extracted specification implies the original software system specification. The two proofs can be tackled with separate specialized techniques.

In order to facilitate both proofs, a variety of semantics-preserving transformations are used to refactor the implementation. These refactorings reduce the complexity of verification caused by program refinements and optimizations that occur in practice. They are either effected or checked mechanically. Refactoring transformations are used to simplify both of the proofs, in some cases making proofs feasible that otherwise would not be.

The introduction of a low-level specification as an intermediate point and the application of semantics-preserving refactorings allow the approach to dovetail with standard development processes more easily than existing approaches to formal verification. In effect, verification in Echo proceeds in a direction opposite to that of traditional verification approaches, exploiting automated reasoning and program transformation to dramatically increase the practicality of verification. Relatively few limitations are imposed on developers and many existing software engineering development methods can continue to be used, yet formal verification and all of its benefits can be applied. The proof structure introduced in Echo is designed to scale for large software systems.

In addition, when combined with other types of analysis such as run-time checks, Echo increases the expressive power of formal verification, allowing whole-system assurance arguments to be constructed for richer properties.