In this paper, the authors introduced a general formal verification approach that consists of the procedures of two refinement steps, specification extraction from the implementation, and implication proof. They believe that this approach is novel since the implication proof is carried out between two abstract specification models, thus avoiding or mitigating the difficulty of the direct compliance proof of a concrete implementation against an abstract formal specification in traditional Floyd-Hoare verification. A preliminary design is described, and preliminary results from an example indicate that their approach is feasible.
Echo: a practical approach to formal verification
2005
10 Seiten, 5 Bilder, 10 Quellen
Aufsatz (Konferenz)
Englisch
The PERF Approach for Formal Verification
British Library Conference Proceedings | 2016
|An approach to formal verification of free-flight separation
Tema Archiv | 2010
|Making formal methods practical
IEEE | 2000
|Making Formal Methods Practical
British Library Conference Proceedings | 2000
|