On Formal Definition and Analysis of Formal Verification Processes
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.
KeywordsFormal Definition Finite State Machine Formal Verification Verification Process Proof Assistant
Unable to display preview. Download preview PDF.
- 1.Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
- 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.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.Futatsugi, K.: Fostering Proof Scores in CafeOBJ. In: Intl. Conference on Formal Engineering Methods, Shanghai, China, pp. 1–20 (2010)Google Scholar
- 8.King, J.C.: A Program Verifier., PhD Thesis, Carnegie Mellon University (1969)Google Scholar
- 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.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.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
- 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.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