TY - JOUR AU - Moroz, Olha AU - Tolstoluzka, Olena PY - 2021/11/29 Y2 - 2024/03/28 TI - Using the methods of formal synthesis and verification of parallel time-parameterized models for solving the system of linear equations by Gaussian elimination JF - Bulletin of V.N. Karazin Kharkiv National University, series «Mathematical modeling. Information technology. Automated control systems» JA - МІА VL - 52 IS - SE - DO - 10.26565/2304-6201-2021-52-07 UR - https://periodicals.karazin.ua/mia/article/view/21417 SP - 52-70 AB - The main solution to the problem of improving the efficiency of parallel computing systems is the methods of formal synthesis of efficient time-parameterized multiparallel models. The article is devoted to investigating the efficiency of using the formal synthesis methods of the given class of parallel models for the specific applied problems. The analysis of methods of parallel data processing and efficiency indicators, as well as the analysis of synthesis methods and means of specification and visualization of parallel static and time-parameterized problem models have been carried out. A parallel time-parameterized model of the Gaussian algorithm based on the method of SCS structures, as well as a parallel time-parameterized model of the Gaussian algorithm based on the method of SCS structures and formal polynomials have been developed. A comparative evaluation of the effectiveness of these two synthesis methods for the criterion of minimizing the number of interprocessor messages in the cluster system. The software implementation for creating parallel time-parameterized models of solving systems of linear equations by Gaussian elimination for cluster systems taking into account the communication component has been developed. The research object is the methods of formal synthesis of parallel time-parameterized models for computing systems with distributed memory (MPP, CLASTER). The research subject is the efficiency of using the methods of formal synthesis of multiparallel time-parameterized models of specific applied problems for the criterion of minimizing the number of interprocessor exchanges in the cluster system. ER -