Geodesic
A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language
Vestnik Ûžno-Uralʹskogo gosudarstvennogo universiteta. Seriâ Vyčislitelʹnaâ matematika i informatika, Tome 4 (2015) no. 2, pp. 58-70 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

The article is devoted to the architecture development of the toolkit for supporting formal verification of functional data-flow parallel programs in the Pifagor Language. The method ofdeduction based on Hoare logic is used for formal verification. A proof process is considered asa tree where each node is a program data-flow graph, whose edges are marked with formulasin a specification language. The tree root is the initial Hoare triple, namely the program data-flow graph with a precondition and a postcondition. In this article basic transformations of thedata-flow graph are considered: edge marking, equivalent transformation, splitting, folding of theprogram. By means of these transformations the initial triple is being transformed and finally isreduced to a set of formulas in the specification language. If all of these formulas are identicallytrue, then the program is correct. Architecture of the toolkit for supporting formal verification offunctional data-flow parallel programs is proposed, which allows to construct a proof three. Theimplementation of the toolkit is introduced and its main functionality is considered.
Keywords: functional data-flow parallel programming, Pifagor programming language, programs formal verification, toolkit for supporting formal verification. 
@article{VYURV_2015_4_2_a4,
     author = {M. S. Ushakova and A. I. Legalov},
     title = {A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language},
     journal = {Vestnik \^U\v{z}no-Uralʹskogo gosudarstvennogo universiteta. Seri\^a Vy\v{c}islitelʹna\^a matematika i informatika},
     pages = {58--70},
     year = {2015},
     volume = {4},
     number = {2},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/VYURV_2015_4_2_a4/}
}
TY  - JOUR
AU  - M. S. Ushakova
AU  - A. I. Legalov
TI  - A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language
JO  - Vestnik Ûžno-Uralʹskogo gosudarstvennogo universiteta. Seriâ Vyčislitelʹnaâ matematika i informatika
PY  - 2015
SP  - 58
EP  - 70
VL  - 4
IS  - 2
UR  - http://geodesic.mathdoc.fr/item/VYURV_2015_4_2_a4/
LA  - ru
ID  - VYURV_2015_4_2_a4
ER  - 
%0 Journal Article
%A M. S. Ushakova
%A A. I. Legalov
%T A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language
%J Vestnik Ûžno-Uralʹskogo gosudarstvennogo universiteta. Seriâ Vyčislitelʹnaâ matematika i informatika
%D 2015
%P 58-70
%V 4
%N 2
%U http://geodesic.mathdoc.fr/item/VYURV_2015_4_2_a4/
%G ru
%F VYURV_2015_4_2_a4
M. S. Ushakova; A. I. Legalov. A toolkit for supporting formal verification of programs in the functional data-flow parallel programming language. Vestnik Ûžno-Uralʹskogo gosudarstvennogo universiteta. Seriâ Vyčislitelʹnaâ matematika i informatika, Tome 4 (2015) no. 2, pp. 58-70. http://geodesic.mathdoc.fr/item/VYURV_2015_4_2_a4/

[1] Nepomnyaschiy V.A., Ryakin O.M., Applied Methods for Programs Verification, Radio i svyaz, M., 1988, 255 pp.

[2] C.A.R. Hoare, “An axiomatic basis for computer programming”, Communications of the ACM, 10:12 (1969), 576–585 | DOI

[3] M. Barnett, B.Y.E. Chang, R. Deline, B. Jacobs, K.R.M. Leino, “Boogie: A modular reusable verifier for object-oriented programs”, Formal Methods for Components and Objects, Lecture Notes in Computer Science, 4111, 2006, 364–387 | DOI

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

[5] J. Van den Berg, B. Jacobs, “The LOOP compiler for Java and JML”, Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, 2031, 2001, 299–312 | DOI | Zbl

[6] W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hähnle, W. Menzel, W. Mostowski, A. Roth, S. Schlager, P.H. Schmitt, “The KeY Tool”, Software and System Modeling, 4:1 (2005), 32–54 | DOI

[7] Legalov A.I., Kuzmin D.A., Kazakov F.A., et al., “An Approach to Portable Parallel Programs”, Open Systems, 2003, no. 5, 36–42

[8] Legalov A.I., “The Functional Programming Language for Creating Architecture-Independent Parallel Programs”, Computational Technologies, 10 (2005), 71–89 | Zbl

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

[10] Kropacheva M.S., “Formalization of the Semantics for the Functional Data-Flow Parallel Language Pifagor”, The Problems of Region Informatization, Proceedings of 12th Russian Scientific-Practical Conference (Krasnoyarsk, Russia, November, 22–23, 2011), Publishing of the Siberian Federal University, Krasnoyarsk, 2011, 144–148

[11] Matkovskiy I.V., “Parallel Event-Based Machine for Functional Dataflow Programming Language «Pifagor»”, Information and Mathematical Technologies in Science and Management, Proceedings of the 17th Baikal Russian Conference with the International Participant (Irkutsk – Baikal, Russia, June, 30 – July, 9, 2012), v. 2, Publishing of the Melentiev Energy Systems Institute of Siberian Branch of the Russian Academy of Sciences, Irkutsk, 2012, 186–193

[12] Legalov, A.I., Savchenko G.V., Vasilev V.S., “Computation Event Model Backing the Execution of Functional Data Flow Concurrent Programs”, Systems. Methods. Technologies, 13:1 (2012), 113–119