UDC 004.4'242
PETRI-NET BASED METHOD OF PARALLEL PROGRAMS FORMAL VERIFICATION
A. N. Ivutin, Ph.D (Tech.), accociate professor, Head of the Department CT, TSU, Tula, Russia;
orcid.org/ 0000-0003-2970-2148, e-mail: This email address is being protected from spambots. You need JavaScript enabled to view it.
A. G. Troshina, Ph.D (Tech.), associate professor, CT department, TSU, Tula, Russia;
orcid.org/ 0000-0002-4304-2513, e-mail: This email address is being protected from spambots. You need JavaScript enabled to view it.
The problem of parallel programs formal verification using mathematical apparatus of the theory of Petri nets is considered. The aim of the work is to formalize methods of parallel program analysis to automate their verification. Correct source sequential program code requires additional verification in connection with the distribution of commands and operations between parallel threads, their coordination and synchronization. The result of incorrect conversion of sequential code to parallel is unpredictable behavior of the program. Thus, the main objective of the work is the development of verification methods, as well as error correction in parallel programs. Based on the theory of Petri nets with additional semantic relations, theorems on the equivalence of parallel and sequential algorithms are formed and proved, error correction methods in parallel algorithms are developed.
Key words: Petri net, parallel program, equivalence of the nets, verification, semantic relations.