The echo approach to formal verification

ABSTRACT

In this research abstract, we propose Echo: a general formal verification approach that combines theorem proving, model checking, and code-level tools to show an implementation's compliance with its formal specification. We believe that this approach is novel since the major proof step 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. We present our prototype design and implementation of the major components of the approach and we instantiate the approach to verify SPARK Ada implementations against PVS specifications. We conducted an initial experiment to determine the feasibility of the approach using a hypothetical avionics system.

REFERENCES

• 1: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 2: Richard Banach , M. Poppleton, Retrenchment: An Engineering Variation on Refinement, Proceedings of the Second International B Conference on Recent Advances in the Development and Use of the B Method, p.129-147, April 22-24, 1998
• 3: John Barnes , J. G. Barnes, High Integrity Software: The SPARK Approach to Safety and Security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
• 4: Barnett, M., K. Rustan M. Leino, and W. Schulte, The Spec# Programming System: An Overview, In CASSIS 2004, LNCS vol. 3362, Springer, 2004.
• 5: R. W. Butler , G. B. Finelli, The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software, IEEE Transactions on Software Engineering, v.19 n.1, p.3-12, January 1993 [doi>10.1109/32.210303]
• 6: Holzmann, G. J., The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, 2003.
• 7: Leavens, G. T. and Y. Cheon, Design by Contract with JML, draft paper, Iowa State University, April 2005.
• 8: Barbara H. Liskov , Jeannette M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.6, p.1811-1841, Nov. 1994 [doi>10.1145/197320.197383]
• 9: Munoz, C., PBS: Support for the B-method in PVS, Tech. Report SRI-CSL-99-01, SRI International, February 1999.
• 10: PVS Specification and Verification System (http://pvs.csl.sri.com/).
• 11: Spivey, J., Understanding Z, Cambridge University Press, 1988.
• 12: Elisabeth A. Strunk , John C. Knight , M. Anthony Aiello, Assured Reconfiguration of Fail-Stop Systems, Proceedings of the 2005 International Conference on Dependable Systems and Networks (DSN'05), p.2-11, June 28-July 01, 2005 [doi>10.1109/DSN.2005.22]
• 13: Elisabeth A. Strunk , Xiang Yin , John C. Knight, Echo: a practical approach to formal verification, Proceedings of the 10th international workshop on Formal methods for industrial critical systems, p.44-53, September 05-06, 2005, Lisbon, Portugal [doi>10.1145/1081180.1081187]
• 14: Michael W. Whalen , Mats P. E. Heimdahl, An Approach to Automatic Code Generation for Safety-Critical Systems, Proceedings of the 14th IEEE international conference on Automated software engineering, p.315, October 12-15, 1999

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability; Formal methods

General Terms:
Reliability, Verification

Keywords:
formal specification, formal verification