Loading...
Please wait, while we are loading the content...
Similar Documents
Echo: a practical approach to formal verification (2005)
| Content Provider | CiteSeerX |
|---|---|
| Author | Yin, Xiang Strunk, Elisabeth Knight, John |
| Description | In Proceedings, Formal Methods for Industrial Critical Systems (FMICS |
| Abstract | 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. In this paper, 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. |
| File Format | |
| Publisher Date | 2005-01-01 |
| Access Restriction | Open |
| Subject Keyword | Abstract Formal Specification Floyd-hoare Pattern Verified Implementation Traditional Formal Verification Approach Generated Specification Ada Code Direct Compliance Argument Floyd-hoare Style Concrete Implementation Human-guided Refinement Spark Ada Spark Annotation Significant Skill Spark Toolset Implementation Language Pvs Specification Preliminary Indication Appropriate Spark Annotation Tedious Direct Compliance Proof General Formal Verification Approach Major Proof Step Safe Operation Annotation Compliance Hypothetical Avionics System |
| Content Type | Text |
