Тechnology of semantic-numerical verification of time-parameterized parallel programs for information and control systems
Abstract
The article analyzes the publications and the latest advancements in the usage of time-parameterized multi-parallel programs in the field of highly effective information technologies, as well as, information and control systems. The object of research is the methods of automatic programming of time-parameterized multi-parallel programs that can process large volumes of data in a short time. The article provides for the definition of time-parameterized multiparallel programs as constructions that correspond to the specification of data objects, operations/functions, static relationships, ordering of operations/functions in the dynamics of a parallel computing process, division into time fragments, division of commands into subsets, and the information about physical data values.
The subject of the study is the effectiveness of using technologies of verification of time-parameterized multi-parallel programs, in particular, using the semantic-numerical specification structure format, that allows formalizing and automating the verification process. The developed technology of semantic-numerical verification of time-parameterized parallel programs for information and control systems provides verification of the syntactic and temporal correctness of the formal synthesis of semantic-numerical specification structures.
The article also presents the conceptual model of the verification technology of time-parameterized parallel programs for information and control systems. The basis for supporting the automatic nature of verification is the semantic-numerical specification structure formed at all stages of synthesis. The formal nature of the verification processes of time-parameterized multiparallel programs is based on the construction of their mathematical models in terms of set theory.
The article will contribute to the further development of research in the field of time-parameterized multiparallel programs.
Downloads
References
/References
Semerenko V.P. Technologies of parallel computing: study guide. Vinnytsia: VNTU, 2018. 104p. [in Ukrainian].
Kuzma K.T., Melnyk O.V. Parallel and distributed computing: a textbook for higher education institutions. Mykolaiv: FOP Shvets V. M., 2020. 172 p. [in Ukrainian].
Kotsovsky V. M. The theory of parallel computing: a textbook. Uzhhorod: PE "AUTDOR-Shark", 2021. 188 p. [in Ukrainian].
Dorogy Y.Yu., Tsurkan V.V. Review of methods of verification of parameterized models. Collection of scientific works of the Admiral Makarov National Shipbuilding University. Mykolaiv: NUK, 2020. No. 1 (479). P. 82–90. [in Ukrainian] URL: http://eir.nuos.edu.ua/handle/123456789/3802. (Last accessed: 28.11.2022).
Tolstoluzkyi, Y., Berdnikov, A., Budko, V., Tolstoluzhskaya, E., & Moroz, O. (2021). Development and verification of SCS network planning model. Bulletin of V.N. Karazin Kharkiv National University, Series «Mathematical Modeling. Information Technology. Automated Control Systems», 51, Р. 81–86. [in Ukrainian] URL: https://doi.org/10.26565/2304-6201-2021-51-09 (Last accessed: 23.10.2022).
Moroz, O., & Tolstoluzka, O. (2021). Using the methods of formal synthesis and verification of parallel time-parameterized models for solving the system of linear equations by Gaussian elimination. Bulletin of V.N. Karazin Kharkiv National University, Series «Mathematical Modeling. Information Technology. Automated Control Systems», 52, Р.52–70. [in Ukrainian] URL: https://doi.org/10.26565/2304-6201-2021-52-07. (Last accessed: 20.11.2022).
Семеренко В. П. Технології паралельних обчислень : навчальний посібник. Вінниця : ВНТУ, 2018. 104 с.
Кузьма К.Т., Мельник О.В. Паралельні та розподілені обчислення: навчальний посібник для вищих закладів освіти. Миколаїв : ФОП Швець В. М., 2020. 172 с.
Коцовський В. М. Теорія паралельних обчислень: навчальний посібник. Ужгород: ПП «АУТДОР-Шарк», 2021. 188 с.
Дорогий Я. Ю., Цуркан В. В. Огляд методів верифікації параметризованих моделей. Збірник наукових праць Національного університету кораблебудування імені адмірала Макарова. Миколаїв : НУК, 2020. № 1 (479). С. 82–90. URI http://eir.nuos.edu.ua/handle/123456789/3802.
Толстолузький Є.Д., Бердніков А.Г., Будько В.В., Толстолузька О. Г., Мороз О. Ю. Розробка та верифікація СЧС моделі мережевого планування. Вісник Харківського національного університету ім. В.Н. Каразіна серія «Математичне моделювання. Інформаційні технології. Автоматизовані системи управління». 2021. Вип. 51. С.81–86. https://doi.org/10.26565/2304-6201-2021-51-09
Ольга Мороз, Олена Толстолузька, Використання методів формального синтезу та веріфікації паралельних часопараметризованих моделей для рішення системи лінійних рівнянь методом Гауса , Вісник Харківського національного університету імені В.Н. Каразіна, серія «Математичне моделювання. Інформаційні технології. Автоматизовані системи управління». 2021. Вип 52 С. 52–70. https://doi.org/10.26565/2304-6201-2021-52-07.
