В роботі досліджено використання інструментальних засобів алгоритмічного етапу проектування для застосунків в технології GPGPU та сформовано формалізовану методику створення паралельних застосувань для програмних систем із відеоадаптерами. На основі проведених досліджень створено комплексний метод проектування та верифікації високопродуктивних застосувань для програмних систем, які включають відеоадаптери для виконання обчислень загального призначення, який дозволяє використати інструментальні засоби алгоритмічного етапу проектування, а саме – алгебри алгоритмів, транзиційні системи, мережеві, автоматні моделі та формули лінійно-темпоральної логіки для підвищення продуктивності паралельних застосувань а також забезпечення їх надійності. До переваг цього методу відносяться можливість моделювання системи, що розглядається, на різних рівнях абстракції, що дозволяє задіяти як дедуктивну верифікацію або класичне тестування на високому рівні абстракції, так і автоматизовані методи верифікації більш низкорівневої логіки, такі, як перевірка моделі. Отриманий метод застосовано для вирішення задачі кластеризації з використанням обчислювальних потужностей графічних адаптерів та верифікації отриманої системи. В ході дослідження було виявлено помилку синхронізації, яку неможливо було б виявити за допомогою традиційного тестування. Побудовано регулярну схему алгоритму Джонсона з використанням математичного апарату САА-М, яка є основною для формування паралельних схем алгоритму з використанням відеоадаптерів та архітектури обчислень CUDA. На основі послідовної параметричної САА-схеми побудовано паралельну САА-М-схему алгоритму Джонсона. Запропоновано метод розпаралелювання алгоритму Джонсона для програмно-апаратної платформи CUDA. Наукова новизна отриманих результатів полягає в тому, що вперше використано апарати систем алгоритмічних алгебр та транзиційних систем для формалізації застосувань в технології GPGPU; створено комплексний метод проектування та верифікації таких застосувань, який дозволяє вирішити проблему складності інженерного проектування застосувань для сучасних гетерогенних систем; апробовано створений метод на прикладах вирішення кількох задач, зокрема задачі кластеризації та задачі пошуку шляхів у графі (алгоритму Джонсона). Отримані результати мають не лише теоретичне, але і практичне значення, оскільки можуть бути використані як для проектування нових, так і для дослідження існуючих застосувань та виявлення в них помилок.^UThe use of tools of the algorithmic design stage for applications in GPGPU technology was investigated in the thesis and the formalized method of parallel application design for massively parallel GPU-based computing systems was created. A comprehensive high-performance application design and verification method for systems that include GPUs to perform general purpose calculations was created. The proposed method allows using the tools of the algorithmic design phase, namely - algebras of algorithms, transition systems, Petri networks, automaton models and formulas of linear-temporal logic to increase the application performance and guarantee its reliability. The advantages of this method include the ability to model the system under analysis at different levels of abstraction, which allows using both deductive verification and classical testing at a high level of abstraction, and automated methods of verification of lower level logic, such as the model verification. The obtained design method is used to solve the problem of clustering using the GPU computing power and verification of the resulting system. The analysis identified a synchronization error that could not be detected by traditional testing. A regular scheme of Johnson's algorithm was built using the SAA-M mathematical apparatus. The scheme served as the basis for the formation of parallel schemes of the algorithm using GPGPU specifics and CUDA architecture. A parallel CAA-M scheme of Johnson's algorithm is constructed on the basis of a sequential parametric CAA scheme. A method of parallelization of the algorithm for the CUDA software and hardware platform is proposed. The scientific novelty of the obtained results is that for the first time the apparatus of systems of algorithmic algebras and transition systems were used to formalize applications in GPGPU technology; a comprehensive application design and verification method was created, which allows to solve the problem of complexity of engineering design of applications for modern heterogeneous systems; the created method was tested on examples of the implementing solutions for several problems, in particular - clustering problem and all pair shortest path graph problem (Johnson's algorithm). The obtained results have not only theoretical but also practical significance, as they can be used both for designing new and for analyzing existing applications to identify potential failure paths in it.