On Formal Definition and Analysis of Formal Verification Processes

  • Leon J. Osterweil
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)

Abstract

This paper suggests that there is considerable value in creating precise and formally-defined specifications of processes for carrying out formal verification, and in then subjecting those processes to rigorous analysis, and using the processes to guide the actual performance of formal verification. The paper suggests that some of the value could derive from widening the community of verifiers by having a process definition guide the performance of formal verification by newcomers or those who may be overawed by the complexities of formal verification. The paper also suggests that formally-defined process definitions can be of value both to novices and more experienced verifiers by serving as subjects of both dynamic and static analyses, with these analyses helping to build the confidence of various stakeholder groups (including the verifiers themselves) in the correct performance of the process and hence the correctness of the verification results. This paper is a status report on early work aimed at developing such processes, and demonstrating the feasibility and value of such analyses. The paper provides an example of a formally-defined verification process and suggests some kinds of dynamic and static analyses of the process. The process incorporates specification of both the nominal, ideal process as well as how the process must be iterated in response to such verification contingencies as incorrect assertions, incorrectly stated lemmas, and failed proofs of lemmas. In demonstrating how static analyses of this process can demonstrate that it assures certain kinds of desirable behaviors, the paper demonstrates an approach to providing effective verification guidance that assures sound verification results.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  2. 2.
    Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)MATHGoogle Scholar
  3. 3.
    Dwyer, M.B., Clarke, L.A., Cobleigh, J.M., Naumovich, G.: Flow Analysis for Verifying Properties of Concurrent Software Systems. ACM Transactions on Software Engineering and Methodology 13(4), 359–430 (2004)CrossRefGoogle Scholar
  4. 4.
    Floyd, R.W.: Assigning Meanings to Programs. In: Schwartz, J.T. (ed.) Proceedings of a Symposium on Applied Mathematics, vol. 19, pp. 19–31 (1967)Google Scholar
  5. 5.
    Futatsugi, K.: Verifying Specifications with Proof Scores in CafeOBJ. In: Intl. Conf. on Automated Software Engineering, Tokyo, Japan, pp. 3–10 (2006)Google Scholar
  6. 6.
    Futatsugi, K.: Fostering Proof Scores in CafeOBJ. In: Intl. Conference on Formal Engineering Methods, Shanghai, China, pp. 1–20 (2010)Google Scholar
  7. 7.
    Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10), 576–580 (1976)CrossRefMATHGoogle Scholar
  8. 8.
    King, J.C.: A Program Verifier., PhD Thesis, Carnegie Mellon University (1969)Google Scholar
  9. 9.
    Osterweil, L.J.: Software Processes are Software Too. In: ACM SIGSOFT/IEEE 9th International Conference on Software Engineering (ICSE 1987), Monterey, CA, pp. 2–13 (March 1987)Google Scholar
  10. 10.
    Osterweil, L.J.: Software Processes Are Software Too, Revisited. In: ACM SIGSOFT/IEEE 19th International Conference on Software Engineering (ICSE 1997), Boston, MA, pp. 540–548 (May 1997)Google Scholar
  11. 11.
    Osterweil, L.J., Clarke, L.A., Podorozhny, R., Wise, A., Boose, E., Ellison, A.M., Hadley, J.: Experience in Using a Process Language to Define Scientific Workflow and Generate Dataset Provenance. In: Proceedings of the ACM SIGSOFT 16th International Symposium on Foundations of Software Engineering, Atlanta, GA, pp. 319–329 (2008)Google Scholar
  12. 12.
    Paulson, L.C.: The foundation of a generic theorem prover. Journal of Automated Reasoning 5(3), 363–397 (1989)MathSciNetCrossRefMATHGoogle Scholar
  13. 13.
    Wise, A.: Little-JIL 1.5 Language Report. Department of Computer Science, University of Massachusetts, Amherst, UM-CS-2006-51 (2006)Google Scholar
  14. 14.
    Wise, A., Cass, A.G., Lerner, B.S., McCall, E.K., Osterweil, L.J., Sutton Jr., S.M.: Using Little-JIL to coordinate agents in software engineering. In: Proceedings of the Automated Software Engineering Conference (ASE 2000), Grenoble, France (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Leon J. Osterweil
    • 1
  1. 1.Lab. For Advanced Software Engineering Research (laser.cs.umas.edu) School of Computer ScienceUniversity of MassachusettsAmherstUSA

Personalised recommendations