Automation of formal verification of programs in the Pifagor language

M. S. Ushakova ; A. I. Legalov

Modelirovanie i analiz informacionnyh sistem, Tome 22 (2015) no. 4, pp. 578-589.

Résumé

Nowadays, due to software sophistication, programs correctness is more often proved by means of formal verification. The method of deduction based on Hoare logic could be used for any programming language and it has the capability of partial automation of the proof process. However, the method of deduction is not widely used for verification of parallel programs because of high complexity of the process. The usage of the functional data-flow paradigm of parallel programming allows to decrease the complexity of the proof process. In this article a proof process of correctness of functional data-flow parallel programs in the Pifagor language is considered. The proof process of a program correctness is considered as a tree where each node is a program data-flow graph, whose edges are marked with formulas in a specification language. The tree root is the initial program data-flow graph with a precondition and a postcondition, which describe restrictions on input variables and correctness conditions of the result of the program execution, respectively. Basic transformations of the data-flow graph are edge marking, equivalent transformation, splitting, folding of the program. By means of these transformations the data-flow graph is transformed and finally is reduced to a set of formulas in the specification language. If all these formulas are identically true, the program is correct. Several modules is distinguished in the system: “Program correctness prover”, “Axioms and theorems library management system” and “Errors analysis and output of information about errors”. According to this architecture, the toolkit for supporting formal verification was developed. The main functionality of the system implementation is considered.

Détail

Keywords: functional data-flow parallel programming, Pifagor programming language, programs formal verification, toolkit for supporting formal verification.

Bibliographie

[1] Nepomnyaschiy V. A., Ryakin O. M., Prikladnyie metodyi verifikatsii programm, Radio i svyaz, M., 1988, 255 pp. (in Russian)

[2] Hoare C. A. R., “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 10:12 (1969), 576–585 | DOI

[3] Floyd R. W., “Assigning meaning to programs”, Proc. of Symposium in Applied Mathematics, Mathematical Aspects of Computer Science, 19, ed. J. T. Schwartz, 1967, 19–32 | DOI | MR | Zbl

[4] Barnett M., Chang B. Y. E., Deline R., et al., “Boogie: A Modular Reusable Verifier for Object-Oriented Programs”, FMCO 2005, LNCS, 4111, 2006, 364–387

[5] Nepomniaschy V. A., Anureev I. S., Atuchin M. M., “C Program Verification in SPECTRUM Multilanguage System”, Automatic Control and Computer Sciences, 45:7 (2011), 413–420 | DOI

[6] Van den Berg J., Jacobs B., “The LOOP compiler for Java and JML”, Tools and Algorithms for the Construction and Analysis of Systems, LNCS, 2031, 2001, 299–312 | Zbl

[7] Ahrendt W., Baar T., Beckert B., “The KeY Tool”, Software and System Modeling, 4:1 (2005), 32–54 | DOI

[8] Detlefs D., Nelson G., Saxe J. B., “Simplify: a theorem prover for program checking”, Journal of the ACM, 52:3 (2005), 365–473 | DOI | MR | Zbl

[9] Owre S., Rajan S., Rushby J. M., “PVS: Combining Specification, Proof Checking, and Model Checking”, Computer-Aided Verification, CAV'96, LNCS, 1102, 1996, 411–414

[10] Legalov A. I., “Funktsionalnyiy yazyik dlya sozdaniya arhitekturno-nezavisimyih parallelnyih programm”, Vyichislitelnyie tehnologii, 10:1 (2005), 71–89 (in Russian) | Zbl

[11] Legalov A. I., Kuzmin D. A., Kazakov F. A., “Na puti k perenosimyim parallelnyim programmam”, Otkryityie sistemyi, 5 (2003), 36–42 (in Russian)

[12] Kropacheva M. S., Legalov A. I., “Formal Verification of Programs in the Functional Data-Flow Parallel Language”, Automatic Control and Computer Sciences, 47:7 (2013), 373–384 | DOI

[13] Kropacheva M. S., Legalov A. I., “Formal Verification of Programs in the Pifagor Language”, Parallel Computing Technologies, 12th International Conference PaCT-2013 (September 30–October 4, 2013, Saint-Petersburg, Russia), LNCS, 7979, 2013, 80–89

[14] Kropacheva M. S., “Formalizatsiya semantiki funktsionalno-potokovogo yazyika parallelnogo programmirovaniya Pifagor”, Problemyi informatizatsii regiona, PIR-2011, Materialyi XII Vserossiyskoy nauchno-prakticheskoy konferentsii (Krasnoyarsk, 22 – 23 noyabrya 2011), Publishing of the Siberian Federal University, Krasnoyarsk, 2011, 144–148 (in Russian)

[15] The Seventeen Provers of the World, AI Systems, LNAI, 3600, ed. Wiedijk F., 2006, 169 pp. | MR

[16] Gordon M., Melham T., Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, 1993 | MR | Zbl

[17] Bertot Y., Casteran P., Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer, 2004, 494 pp. | MR

[18] Nipkow T., Paulson L., Wenzel M., Isabelle/HOL — A Proof Assistant for Higher-Order Logic, LNCS, 2283, 2002, 205 pp. | MR | Zbl

[19] Legalov A. I., Savchenko G. V., Vasilev V. S., “Sobyitiynaya model vyichisleniy, podderzhivayuschaya vyipolnenie funktsionalno-potokovyih parallelnyih programm”, Sistemyi. Metodyi. Tehnologii, 1:13 (2012), 113–119 (in Russian)

[20] Matkovskiy I. V., “Parallelnaya sobyitiynaya mashina dlya funktsionalno-potokovogo yazyika “Pifagor””, Informatsionnyie i matematicheskie tehnologii v nauke i upravlenii, Sbornik trudov XVVII Baykalskoy Vserossiyskoy konferentsii s mezhdunarodnyim uchastiem (Irkutsk – Baykal, 30 iyunya – 9 iyulya 2012), v. 2, Publishing of the Melentiev Energy Systems Institute of Siberian Branch of the Russian Academy of Sciences, Irkutsk, 2012, 186–193 (in Russian)