Open AccessAnalysis of existing parallel programs verification technologies
Author(s) -
© Moroz,
Olena G. Tolstoluzka,
R Savchenko,
Olha Moroz,
R Savchenko Moroz,
Olha Yuriivna,
Tolstoluzka Gennadiivna,
Savchenko Valeriyovich
Publication year - 2020
Publication title -
vìsnik harkìvsʹkogo nacìonalʹnogo unìversitetu ìmenì v.n. karazìna. serìâ matematične modelûvannâ, ìnformacìjnì tehnologìï, avtomatizovanì sistemi upravlìnnâ
Language(s) - English
Resource type - Journals
eISSN - 2524-2601
pISSN - 2304-6201
DOI - 10.26565/2304-6201-2020-46-07
Subject(s) - computer science , debugging , software verification , formal methods , formal verification , software , functional verification , verification , verification and validation , software engineering , runtime verification , software system , software construction , programming language , statistics , mathematics
The past few decades have seen large uctuations in the perceived value of parallel computing. At times, parallel computation has optimistically been viewed as the solution to all of our computational limitations. The conventional division of verification methods is analyzed. It is concluded that synthetic methods of software verification can be considered as the most relevant, most useful and productive ones. It is noted that the implementation of the methods of formal verification of software of computer systems, which supplement the traditional methods of testing and debugging, and make it possible to improve the uptime and security of programs, is relevant. Methods of computer systems software formal verification can guarantee the check that verified properties are performed by system model. Nowadays, these methods are actively being developed in the direction of reducing the formal verification total cost, support of modern programming concepts and minimization of "manual" work in the transition from the system model to its implementation. Their main feature is an ability to search for errors using mathematical model, without recourse to existing realization of software. It is very convenient and economical. There are several specific techniques used for formal models analysis, such as deductive analysis, model and consistence check. Every verification method is been used in particular cases, depending on the goal. Synthetic methods of software verification are considered the most actual, useful and efficient, as they somehow try to combine the advantages of different verification approaches, getting rid of their drawbacks. Currently, there has been made significant progress in the development of such methods and their implementation in the practice of industrial software development.