Abstract:
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.
Fulltext:
PDF file (1054 kB)