Echo

From Dependability

Safe operation is crucial to safety-critical systems, and formally verified implementations are desirable. Traditional formal verification approaches follow the Floyd-Hoare style, setting up a direct compliance argument between an abstract formal specification and a concrete implementation. Such approaches require proofs of large numbers of verification conditions. The process of generating and proving verification conditions can require significant skill and can be time-consuming. We introduce a general formal verification approach that closely models the Floyd-Hoare pattern, yet avoids the tedious direct compliance proof between the formal specification and the implementation. The approach moves the major proof step to a point between two abstract specifications. Our preliminary design takes PVS as our specification language and SPARK Ada as our implementation language. We first use a human-guided refinement to manually generate Ada code along with appropriate SPARK annotations from a PVS specification. We then verify the annotations’ compliance with the specification by (1) mechanically extracting a PVS specification from them, and (2) proving that properties of the generated specification imply all of the properties of the original. We rely on the existing SPARK toolset to verify the Ada code against the SPARK annotations. The process is largely automatic or computer-aided. A case study using a hypothetical avionics system provides a preliminary indication that this approach is feasible and practical.

Selected Papers

• Strunk, Elisabeth A., Xiang Yin, and John C. Knight

Echo: A Practical Approach to Formal Verification

FMICS-05: Tenth International Workshop on Formal Methods for Industrial Critical Systems, September 2005 (PDF)