Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах
Запропоновано методологію проєктування застосунків для систем із масовим паралелізмом на прикладі GPGPU-систем, орієнтовану на алгоритмічний етап проєктування. Розглянуто два етапи проєктування: створення формальної специфікації та її дослідження і верифікація. Для першого етапу запропоновано викори...
Збережено в:
| Опубліковано в: : | Кибернетика и системный анализ |
|---|---|
| Дата: | 2020 |
| Автори: | , |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2020
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/190444 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах / С.Д. Погорілий, М.С. Слинько // Кибернетика и системный анализ. — 2020. — Т. 56, № 4. — С. 196–202. — Бібліогр.: 9 назв. — укр. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-190444 |
|---|---|
| record_format |
dspace |
| spelling |
Погорілий, С.Д. Слинько, М.С. 2023-06-06T17:17:38Z 2023-06-06T17:17:38Z 2020 Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах / С.Д. Погорілий, М.С. Слинько // Кибернетика и системный анализ. — 2020. — Т. 56, № 4. — С. 196–202. — Бібліогр.: 9 назв. — укр. 1019-5262 https://nasplib.isofts.kiev.ua/handle/123456789/190444 004.4 Запропоновано методологію проєктування застосунків для систем із масовим паралелізмом на прикладі GPGPU-систем, орієнтовану на алгоритмічний етап проєктування. Розглянуто два етапи проєктування: створення формальної специфікації та її дослідження і верифікація. Для першого етапу запропоновано використання математичних апаратів системи алгоритмічних алгебр/модифікованої системи алгоритмічних алгебр та транзиційних систем. Для другого етапу проаналізовано використання мережевих та автоматних моделей і наведено переваги кожної моделі. Зокрема, проведено дослідження моделі обчислень в архітектурі NVIDIA CUDA за допомогою мереж Петрі, а також формул лінійно-темпоральної логіки та автоматної моделі. Предложена методология проектирования приложений для систем с массовым параллелизмом на примере GPGPU-систем, ориентированная на алгоритмический этап проектирования. Рассмотрены две фазы проектирования: создание формальной спецификации и ее исследование и верификация. Для первого этапа предложено использование математических аппаратов системы алгоритмических алгебр/модифицированной системы алгоритмических алгебр и транзиционных систем. Для второго этапа проанализировано использование сетевых и автоматных моделей и приведены преимущества каждой из них. В частности, проведено исследование модели вычислений в архитектуре NVIDIA CUDA при помощи сетей Петри, а также формул линейно-темпоральной логики и автоматных моделей. An application design methodology for massively parallelized systems (GPGPU systems) focused on the algorithmic design phase is proposed. Two design sub-steps are considered: creation of the formal specification of the system; and its research and verification. The use of mathematical apparatuses SAA/SAA-M as well as transition systems is proposed for the first step. Advantages and specifics of using network and automaton models for the second step are given. NVIDIA CUDA architecture computation model analysis is proposed using Petri nets (network model) and using linear-temporal logic formulas and Buchi automaton (automaton model). uk Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Нові засоби кібернетики, інформатики, обчислювальної техніки та системного аналізу Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах Методы моделирования и верификации для проектирования приложений в гетерогенных архітектурах Modeling and verification methods for application design in heterogeneous architectures Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| spellingShingle |
Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах Погорілий, С.Д. Слинько, М.С. Нові засоби кібернетики, інформатики, обчислювальної техніки та системного аналізу |
| title_short |
Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| title_full |
Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| title_fullStr |
Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| title_full_unstemmed |
Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| title_sort |
методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| author |
Погорілий, С.Д. Слинько, М.С. |
| author_facet |
Погорілий, С.Д. Слинько, М.С. |
| topic |
Нові засоби кібернетики, інформатики, обчислювальної техніки та системного аналізу |
| topic_facet |
Нові засоби кібернетики, інформатики, обчислювальної техніки та системного аналізу |
| publishDate |
2020 |
| language |
Ukrainian |
| container_title |
Кибернетика и системный анализ |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| format |
Article |
| title_alt |
Методы моделирования и верификации для проектирования приложений в гетерогенных архітектурах Modeling and verification methods for application design in heterogeneous architectures |
| description |
Запропоновано методологію проєктування застосунків для систем із масовим паралелізмом на прикладі GPGPU-систем, орієнтовану на алгоритмічний етап проєктування. Розглянуто два етапи проєктування: створення формальної специфікації та її дослідження і верифікація. Для першого етапу запропоновано використання математичних апаратів системи алгоритмічних алгебр/модифікованої системи алгоритмічних алгебр та транзиційних систем. Для другого етапу проаналізовано використання мережевих та автоматних моделей і наведено переваги кожної моделі. Зокрема, проведено дослідження моделі обчислень в архітектурі NVIDIA CUDA за допомогою мереж Петрі, а також формул лінійно-темпоральної логіки та автоматної моделі.
Предложена методология проектирования приложений для систем с массовым параллелизмом на примере GPGPU-систем, ориентированная на алгоритмический этап проектирования. Рассмотрены две фазы проектирования: создание формальной спецификации и ее исследование и верификация. Для первого этапа предложено использование математических аппаратов системы алгоритмических алгебр/модифицированной системы алгоритмических алгебр и транзиционных систем. Для второго этапа проанализировано использование сетевых и автоматных моделей и приведены преимущества каждой из них. В частности, проведено исследование модели вычислений в архитектуре NVIDIA CUDA при помощи сетей Петри, а также формул линейно-темпоральной логики и автоматных моделей.
An application design methodology for massively parallelized systems (GPGPU systems) focused on the algorithmic design phase is proposed. Two design sub-steps are considered: creation of the formal specification of the system; and its research and verification. The use of mathematical apparatuses SAA/SAA-M as well as transition systems is proposed for the first step. Advantages and specifics of using network and automaton models for the second step are given. NVIDIA CUDA architecture computation model analysis is proposed using Petri nets (network model) and using linear-temporal logic formulas and Buchi automaton (automaton model).
|
| issn |
1019-5262 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/190444 |
| citation_txt |
Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах / С.Д. Погорілий, М.С. Слинько // Кибернетика и системный анализ. — 2020. — Т. 56, № 4. — С. 196–202. — Бібліогр.: 9 назв. — укр. |
| work_keys_str_mv |
AT pogoríliisd metodimodelûvannâíverifíkacíídlâproêktuvannâzastosunkívugeterogenniharhítekturah AT slinʹkoms metodimodelûvannâíverifíkacíídlâproêktuvannâzastosunkívugeterogenniharhítekturah AT pogoríliisd metodymodelirovaniâiverifikaciidlâproektirovaniâpriloženiivgeterogennyharhítekturah AT slinʹkoms metodymodelirovaniâiverifikaciidlâproektirovaniâpriloženiivgeterogennyharhítekturah AT pogoríliisd modelingandverificationmethodsforapplicationdesigninheterogeneousarchitectures AT slinʹkoms modelingandverificationmethodsforapplicationdesigninheterogeneousarchitectures |
| first_indexed |
2025-11-25T22:29:34Z |
| last_indexed |
2025-11-25T22:29:34Z |
| _version_ |
1850564035915808768 |
| fulltext |
ÓÄÊ 004.4
Ñ.Ä. ÏÎÃÎвËÈÉ, Ì.Ñ. ÑËÈÍÜÊÎ
ÌÅÒÎÄÈ ÌÎÄÅËÞÂÀÍÍß ² ÂÅÐÈÔ²ÊÀÖ²¯ ÄËß ÏÐΪÊÒÓÂÀÍÍß
ÇÀÑÒÎÑÓÍÊ²Â Ó ÃÅÒÅÐÎÃÅÍÍÈÕ ÀÐÕ²ÒÅÊÒÓÐÀÕ
Àíîòàö³ÿ. Çàïðîïîíîâàíî ìåòîäîëîã³þ ïðîºêòóâàííÿ çàñòîñóíê³â äëÿ ñèñòåì
³ç ìàñîâèì ïàðàëåë³çìîì íà ïðèêëàä³ GPGPU-ñèñòåì, îð³ºíòîâàíó íà àëãî-
ðèòì³÷íèé åòàï ïðîºêòóâàííÿ. Ðîçãëÿíóòî äâà åòàïè ïðîºêòóâàííÿ: ñòâîðåí-
íÿ ôîðìàëüíî¿ ñïåöèô³êàö³¿ òà ¿¿ äîñë³äæåííÿ ³ âåðèô³êàö³ÿ. Äëÿ ïåðøîãî
åòàïó çàïðîïîíîâàíî âèêîðèñòàííÿ ìàòåìàòè÷íèõ àïàðàò³â ñèñòåìè àëãî-
ðèòì³÷íèõ àëãåáð/ìîäèô³êîâàíî¿ ñèñòåìè àëãîðèòì³÷íèõ àëãåáð òà òðàíçè-
ö³éíèõ ñèñòåì. Äëÿ äðóãîãî åòàïó ïðîàíàë³çîâàíî âèêîðèñòàííÿ ìåðåæåâèõ
òà àâòîìàòíèõ ìîäåëåé ³ íàâåäåíî ïåðåâàãè êîæíî¿ ìîäåë³. Çîêðåìà, ïðîâå-
äåíî äîñë³äæåííÿ ìîäåë³ îá÷èñëåíü â àðõ³òåêòóð³ NVIDIA CUDA çà äîïî-
ìîãîþ ìåðåæ Ïåòð³, à òàêîæ ôîðìóë ë³í³éíî-òåìïîðàëüíî¿ ëîã³êè òà àâòî-
ìàòíî¿ ìîäåë³.
Êëþ÷îâ³ ñëîâà: òðàíçèö³éí³ ñèñòåìè, ñèñòåìè àëãîðèòì³÷íèõ àëãåáð,
GPGPU-ñèñòåìè, ìåðåæ³ Ïåòð³.
ÂÑÒÓÏ
Ñêëàäí³ñòü ïðîãðàìíîãî çàáåçïå÷åííÿ íàáëèæàºòüñÿ äî ìåæ³ ëþäñüêîãî ðî-
çóì³ííÿ, à îòæå, äî ìåæ³ êåðîâàíîñò³. Ñó÷àñí³ òåíäåíö³¿ â ãàëóç³ âèñîêîïðîäóê-
òèâíèõ îá÷èñëåíü çì³ùóþòüñÿ â³ä çàñòîñóâàííÿ êëàñòåð³â, ùî ñêëàäàþòüñÿ ç ìî-
äóë³â çàãàëüíîãî ïðèçíà÷åííÿ, äî âèêîðèñòàííÿ á³ëüø ñïåö³àë³çîâàíèõ êîìïî-
íåíò³â-àêñåëåðàòîð³â (òîáòî â³ä óí³âåðñàëüíèõ öåíòðàëüíèõ ïðîöåñîð³â (ÑPU) äî
³íøèõ áëîê³â — â³äåîàäàïòåð³â íà îñíîâ³ ãðàô³÷íèõ ïðîöåñîð³â (GPU), ïðîãðàìî-
âàíèõ âåíòèëüíèõ ìàòðèöü (FPGA) òîùî), ³íøèìè ñëîâàìè — äî ìåíø ôóíêö³î-
íàëüíèõ ³ ìåíø åíåðãîâèòðàòíèõ ìîäóë³â. Çîêðåìà, ó ðîáîòàõ [1, 2] ðîçãëÿíóòî
âèêîðèñòàííÿ GPU-àêñåëåðàòîð³â äëÿ îá÷èñëåííÿ íåãðàô³÷íèõ çàâäàíü.
Ñòâîðåííÿ ñèñòåì âèñîêîãî ð³âíÿ ñêëàäíîñò³ ç ìàñîâèì ïàðàëåë³çìîì íà
îñíîâ³ â³äåîàäàïòåð³â ïîòðåáóº ðîçðîáëåííÿ íîâ³òí³õ íàóêîâèõ ìåòîä³â îá´ðóí-
òóâàííÿ ÿê àðõ³òåêòóð òàêèõ ñèñòåì, òàê ³ çàñòîñóíê³â äëÿ íèõ. Îñê³ëüêè ñó÷àñí³
áàãàòîïîòîêîâ³ çàñòîñóíêè íàë³÷óþòü ñîòí³ òèñÿ÷ ³ ì³ëüéîíè ïîòîê³â, ðîçâ’ÿçàííÿ
çàäà÷ ïàðàëåë³çàö³¿ äëÿ òàêîãî êëàñó ñèñòåì óíåìîæëèâëþº ³íæåíåðíå ïðîºêòó-
âàííÿ ³ âèìàãຠíàÿâíîñò³ ôîðìàëüíèõ ìåòîä³â, âèêîðèñòàííÿ ìàòåìàòè÷íîãî
àïàðàòà ³ ñïîñîá³â îá´ðóíòóâàííÿ ïðèéíÿòèõ ð³øåíü.
Ðîçðîáíèê, ÿêèé ïðàöþº ó òàêîìó ñåðåäîâèù³, ìຠðîâ’ÿçàòè íèçêó ñêëàäíèõ
çàäà÷. Ç îäíîãî áîêó, äîìåííó ëîã³êó çàñòîñóíêó íå âàðòî æîðñòêî ïðèâ’ÿçóâàòè
äî îá÷èñëþâàëüíî¿ àðõ³òåêòóðè, îñê³ëüêè öå çíèçèòü ñòóï³íü ãíó÷êîñò³ îòðèìàíî¿
ñèñòåìè. Ç ³íøîãî áîêó, ï³ä ÷àñ åêñïåðèìåíòàëüíî¿ ðåàë³çàö³¿ ñèñòåìè ïîòð³áíî
êîíêðåòèçóâàòè çàñòîñóíîê äëÿ òîãî, ùîá ìàêñèìàëüíî ñêîðèñòàòèñÿ ïåðåâàãàìè
òà îñîáëèâîñòÿìè êîíêðåòíî¿ àðõ³òåêòóðè. Ó ö³é ðîáîò³ çàïðîïîíîâàíî ìåòîäî-
ëîã³þ ïðîºêòóâàííÿ ñèñòåì, ÿêà íàäຠçìîãó ðîçâ’ÿçàòè ö³ çàäà÷³ íà àëãî-
ðèòì³÷íîìó åòàï³ ïðîºêòóâàííÿ, òîáòî ùå äî åòàïó åêñïåðèìåíòàëüíî¿ ðåàë³çàö³¿.
 îñíîâó ö³º¿ ìåòîäîëî㳿 ïîêëàäåíî ñèñòåìó àëãîðèòì³÷íèõ àëãåáð Ãëóøêîâà,
òðàíçèö³éí³ ñèñòåìè, ìåòîä ïåðåâ³ðêè íà ìîäåë³ (model checking) òà ïðàâèëà
ë³í³éíî-òåìïîðàëüíî¿ ëîã³êè, à òàêîæ ìåðåæ³ Ïåòð³.
196 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 4
© Ñ.Ä. Ïîãîð³ëèé, Ì.Ñ. Ñëèíüêî, 2020
ÑÒÂÎÐÅÍÍß ÔÎÐÌÀËÜÍί ÑÏÅÖÈÔ²ÊÀÖ²¯ ÏÐΪÊÒÎÂÀÍί ÑÈÑÒÅÌÈ
Äëÿ ôîðìàë³çîâàíîãî ïðåäñòàâëåííÿ àëãîðèòì³â ôóíêö³îíóâàííÿ àáñòðàêòíî¿
ìîäåë³ åëåêòðîííî-îá÷èñëþâàëüíî¿ ìàøèíè (ÅÎÌ) Â.Ì. Ãëóøêîâ çàïðîïîíó-
âàâ ìàòåìàòè÷íèé àïàðàò ñèñòåìè àëãîðèòì³÷íèõ (ì³êðîïðîãðàìíèõ) àëãåáð
(ÑÀÀ). Ïåðåâàãîþ ÑÀÀ (ïîð³âíÿíî ç êëàñè÷íèì ìàòåìàòè÷íèì àïàðàòîì) º ¿¿
îð³ºíòîâàí³ñòü íà ïðîºêòóâàííÿ àëãîðèòì³â ³ ïîäàííÿ àëãîðèòìó ó âèãëÿä³
ôîðìóëè, ùî íàäຠçìîãó çîñåðåäèòèñÿ íà êîíöåïö³ÿõ òà ìåòîäàõ òðàíñôîð-
ìàö³¿ ïàðàëåëüíèõ ñõåì àëãîðèòì³â, àáñòðàãóþ÷èñü â³ä êîíêðåòíèõ äåòàëåé
ïðîãðàìíî¿ ðåàë³çàö³¿. Âèêîðèñòàííÿ ÑÀÀ äຠìîæëèâ³ñòü ôîðìàë³çóâàòè
ëîã³êó ðîáîòè àëãîðèòìó ó òàêèé ñïîñ³á, ùî ìîæíà àáñòðàãóâàòèñÿ â³ä êîí-
êðåòíî¿ îá÷èñëþâàëüíî¿ àðõ³òåêòóðè òà ðîçãëÿäàòè ¿õ ÿê îêðåì³ âèïàäêè á³ëüø
çàãàëüíî¿ àáñòðàêòíî¿ ñõåìè. Äî òîãî æ, îòðèìàí³ ñõåìè ñëóãóþòü äîêóìåí-
òàö³ºþ òà òåîðåòè÷íîþ áàçîþ äëÿ â³äïîâ³äíîãî ïðîãðàìíîãî çàáåçïå÷åííÿ.
Ô³êñîâàíà ÑÀÀ ÿâëÿº ñîáîþ äâîîñíîâíó àëãåáðà¿÷íó ñèñòåìó, â îñíîâó ÿêî¿
ïîêëàäåíî ìíîæèíó îïåðàòîð³â ³ ìíîæèíó óìîâ [3]. Âèêîðèñòàííÿ ÑÀÀ
ÿê ôîðìàë³çîâàíîãî ìåòîäó ïðîºêòóâàííÿ ´ðóíòóºòüñÿ íà òåîðåì³ Ãëóøêîâà,
ÿêà ñòâåðäæóº, ùî äëÿ äîâ³ëüíîãî àëãîðèòìó ³ñíóº (ó çàãàëüíîìó âèïàäêó íå
ºäèíà) ÑÀÀ, â ÿê³é öåé àëãîðèòì ìîæå áóòè ïðåäñòàâëåíèé ðåãóëÿðíîþ ñõå-
ìîþ. ²íøèìè ñëîâàìè, ÿêùî âèçíà÷èòè îñíîâè ÑÀÀ äëÿ êîíêðåòíîãî àëãîðèò-
ìó, ìîæíà ïðåäñòàâèòè öåé àëãîðèòì ó âèãëÿä³ ñõåìè ³ çä³éñíþâàòè ïîäàëüø³
òðàíñôîðìàö³¿ òà îïòèì³çàö³þ âæå íå ç àëãîðèòìîì, à ç éîãî ïðåäñòàâëåííÿì
ó âèãëÿä³ ÑÀÀ-ñõåìè. Ó ðîáîòàõ [4–6] ïðî³ëþñòðîâàíî çä³éñíåííÿ ëàíöþæêà
åêâ³âàëåíòíèõ òðàíñôîðìàö³é ó ñõåìàõ àëãîðèòì³â Äàíöèãà òà Äæîíñîíà íà
îñíîâ³ ìîäèô³êîâàíèõ ñèñòåì àëãîðèòì³÷íèõ àëãåáð (ÑÀÀ-Ì).
Âèêîðèñòàííÿ ñõåì àëãîðèòì³â íàäຠçìîãó îòðèìàòè ìîäåëü ñèñòåìè ïåð-
øîãî ð³âíÿ. Âò³ì, çàñòîñóíîê áóäå ðåàë³çîâàíî íà îñíîâ³ êîíêðåòíî¿ îá÷èñëþ-
âàëüíî¿ àðõ³òåêòóðè, òîìó ïîòð³áíî îá´ðóíòóâàòè êîðåêòí³ñòü òà íàä³éí³ñòü ìî-
äåë³ ñàìå â ìåæàõ ö³º¿ àðõ³òåêòóðè. Ðîçâ’ÿçàííÿ çàäà÷³ ùîäî îá´ðóíòóâàííÿ êî-
ðåêòíîñò³ º íåòðèâ³àëüíèì, îñîáëèâî ÿêùî îá÷èñëþâàëüíà àðõ³òåêòóðà º
ãåòåðîãåííîþ ç ìàñîâèì ïàðàëåë³çìîì (íàïðèêëàä, ÿê ó òåõíîëî㳿 General
Purpose GPU (GPGPU)). Ó ðàç³ âèêîðèñòàííÿ òðàäèö³éíèõ ìåòîä³â ðîçðîáëåííÿ
ïðîãðàì îñíîâíèì ìåòîäîì çàáåçïå÷åííÿ êîðåêòíîñò³ º òåñòóâàííÿ. Ïðîòå, çà
ñëîâàìè Åäñãåðà Äåéêñòðè, òåñòóâàííÿ ìîæå ïîêàçàòè íàÿâí³ñòü ïîìèëîê, àëå íå
ìîæå ãàðàíòóâàòè ¿õíþ â³äñóòí³ñòü [7]. Äî òîãî æ, ï³ä ÷àñ òåñòóâàííÿ íå ìîæíà
âèÿâèòè òèïîâ³ ïîìèëêè ñèíõðîí³çàö³¿ ïàðàëåëüíèõ ïðîãðàì: ïîìèëêè â íèõ ìî-
æóòü çáåð³ãàòèñÿ ðîêàìè ³ âèÿâëÿòèñÿ ï³ñëÿ òðèâàëî¿ åêñïëóàòàö³¿ ÿê ðåàêö³ÿ íà
ñïåöèô³÷íó êîìá³íàö³þ áàãàòüîõ ôàêòîð³â, íàïðèêëàä, íåïåðåäáà÷óâàíèõ øâèä-
êîñòåé âèêîíàííÿ îêðåìèõ ïàðàëåëüíèõ ïðîöåñ³â. Íàâ³òü ÿêùî ìåõàí³çì
ôóíêö³îíóâàííÿ êîæíîãî êîìïîíåíòà ñèñòåìè, ñïðîºêòîâàíî¿ íà îñíîâ³ ìîäåë³
ìàñîâîãî ïàðàëåë³çìó, º àáñîëþòíî çðîçóì³ëèì, ëþäèí³ âàæêî îñÿãíóòè ðîáîòó
âñ³º¿ ñèñòåìè, ïðîöåñè ÿêî¿ º âçàºìîïîâ’ÿçàíèìè.
Çðó÷íèì çàñîáîì ìîäåëþâàííÿ ïðîºêòîâàíî¿ ñèñòåìè º àïàðàò òðàíçèö³éíèõ
ñèñòåì (ÒÑ). Õî÷à ÑÀÀ ³ íàäàþòü çìîãó îñÿãíóòè ñòðóêòóðó çàñòîñóíêó òà
çä³éñíþâàòè åêâ³âàëåíòí³ ïåðåòâîðåííÿ ñõåìè çàñòîñóíêó áåç ïðèâ’ÿçóâàííÿ äî
àïàðàòíî¿ àðõ³òåêòóðè, ïðîòå âîíè íå çàáåçïå÷óþòü ìîæëèâîñò³ òåìïîðàëüíîãî
ìîäåëþâàííÿ òà ãëèáîêîãî àíàë³çó. Çàòå ìîäåë³, ñòâîðåí³ çà äîïîìîãîþ àïàðàòó
ÒÑ, ìîæíà ëåãêî êîíâåðòóâàòè â ³íø³ ôîðìàòè, ÿê³ ï³äòðèìóþòü òåìïîðàëüíó
ëîã³êó, íàïðèêëàä, ìåðåæ³ Ïåòð³. Êð³ì òîãî, ïåðåâàãîþ ÒÑ º ìîæëèâ³ñòü ñòâîðåí-
íÿ ìîäåëåé ð³çíîãî ð³âíÿ ñêëàäíîñò³ çàëåæíî â³ä ðîçâ’ÿçóâàíî¿ çàäà÷³.
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 4 197
Îçíà÷åííÿ 1. Ïðîñòîþ òðàíçèö³éíîþ ñèñòåìîþ [8] íàçèâàºòüñÿ ÷åòâ³ðêà
A S R� ( , , , )� � , äå S — ñê³í÷åííà àáî íåñê³í÷åííà ìíîæèíà ñòàí³â; R — ñê³í÷åí-
íà àáî íåñê³í÷åííà ìíîæèíà ïåðåõîä³â; � �, — äâà â³äîáðàæåííÿ ³ç R â S , ùî
ñòàâëÿòü ó â³äïîâ³äí³ñòü êîæíîìó ïåðåõîäó t R� äâà ñòàíè �( )t òà �( )t , ÿê³ íàçè-
âàþòüñÿ â³äïîâ³äíî ïî÷àòêîì ³ ê³íöåì ïåðåõîäó t .
Îçíà÷åííÿ 2. Çàãàëüíîþ òðàíçèö³éíîþ ñèñòåìîþ (ÇÒÑ) íàçèâàºòüñÿ ÒÑ
A S X R s AP L� ( , , , , , )0 , äå S — ìíîæèíà ñòàí³â; X — ìíîæèíà ä³é, àñîö³éîâà-
íèõ ç ïåðåõîäàìè; R S X S� � � — â³äíîøåííÿ ïåðåõîä³â; s0 — ïî÷àòêîâèé ñòàí
ÇÒÑ; ÀÐ — ìíîæèíà ïðîïîçèö³éíèõ ôîðìóë, àñîö³éîâàíèõ ç³ ñòàíàìè;
L S B AP: ( )� — ôóíêö³ÿ ïîçíà÷îê ñòàí³â, äå B AP( ) — áóëåàí ìíîæèíè ÀÐ.
²íòåãðàö³ÿ ÒÑ ó ö³ë³ñíó ñèñòåìó, ÿêà îðãàí³çîâóº ðîáîòó âñ³õ ÒÑ, âèêî-
íóºòüñÿ çàëåæíî â³ä õàðàêòåðó ïîòð³áíî¿ âçàºìî䳿 ñêëàäîâèõ (ñèíõðîííà, àñèí-
õðîííà, ïàðàëåëüíà, ïîñë³äîâíà). Ö³ ñïîñîáè âçàºìî䳿 óçàãàëüíþþòü îïåðàö³ºþ
ñèíõðîííîãî äîáóòêó ÒÑ. Âèçíà÷åííÿ ñèíõðîííîãî äîáóòêó ÒÑ òà ïðèêëàä éîãî
ïîáóäîâè íàâåäåíî â [1]. Çàñòîñóâàííÿ ÒÑ, ÿê³ îïèñóþòü ñêëàäîâ³ êîìïîíåíòè
ïðîºêòîâàíî¿ ñèñòåìè, à òàêîæ âèçíà÷åííÿ ïðîòîêîëó ¿õíüî¿ âçàºìî䳿 (îáìåæåí-
íÿ ñèíõðîí³çàö³¿ äîáóòêó ÒÑ) íàäຠçìîãó îòðèìàòè âèñîêîð³âíåâó ñïåöèô³êàö³þ
ñèñòåìè (ìîäåëü çàãàëüíîãî òèïó). Ìàþ÷è âèùåçàçíà÷åíó ìîäåëü, ìîæíà ïðèñòó-
ïàòè äî ïðîöåñó ¿¿ âåðèô³êàö³¿. Îñíîâíèìè ìîäåëÿìè òàêîãî ïðîöåñó º àâòîìàòí³
òà ìåðåæåâ³ ìîäåë³, à øëÿõè àíàë³çó ðîçãëÿíóòî â íàñòóïíèõ ðîçä³ëàõ ðîáîòè.
ÂÈÊÎÐÈÑÒÀÍÍß ÌÅÐÅÆÅÂÈÕ ÌÎÄÅËÅÉ ÄËß ÂÅÐÈÔ²ÊÀÖ²¯ ÑÏÅÖÈÔ²ÊÀÖ²¯
Âèêîðèñòàííÿ ÒÑ ÿê ìîäåë³ ñèñòåìè âèñîêîãî ð³âíÿ ñêëàäíîñò³ íàäຠçìîãó
ñòâîðþâàòè àáñòðàêö³¿ ð³çíèõ ð³âí³â (çà ðàõóíîê ð³âíÿ äåòàë³çàö³¿, âèáîðó ôîð-
ìàëüíî¿ ëîã³÷íî¿ ìîâè äëÿ îïèñó ñïåöèô³êàö³é òîùî), êîìïîçèö³¿ ÿêèõ ìîæíà
òðàíñëþâàòè â ìåðåæ³ Ïåòð³ (ÌÏ) ³ äîñë³äæóâàòè çà äîïîìîãîþ çàñîá³â ÌÏ.
Íàãàäàºìî, ùî ñó÷àñí³ ãåòåðîãåíí³ îá÷èñëþâàëüí³ àðõ³òåêòóðè ç âèêîðèñòàí-
íÿì â³äåîàäàïòåð³â îïåðóþòü áàãàòüìà ãðóïàìè ïîòîê³â îäíî÷àñíî, òîìó âèêî-
íàííÿ çàñòîñóíêó ìຠñèíõðîííî-àñèíõðîííèé õàðàêòåð, îñê³ëüêè ð³çí³
³íñòðóêö³¿ ìîæóòü ìàòè ð³çíó òðèâàë³ñòü ÷àñó âèêîíàííÿ ³ íå ïîâåðíóòüñÿ îä-
íî÷àñíî â ì³ñöå ñèíõðîí³çàö³¿. Òîìó äîö³ëüíèì º âèêîðèñòàííÿ ñàìå àïàðàòó
ìåðåæ Ïåòð³.
Ó [8] ïîêàçàíî, ùî ñåìàíòèêà äîáóòêó ÒÑ ³ ñåìàíòèêà ÌÏ, ÿêà éîãî ìîäå-
ëþº, º óçãîäæåíèìè â òîìó ñåíñ³, ùî ïîñë³äîâí³ñòü ãëîáàëüíèõ ïåðåõîä³â
t tk1, ,� ÿâëÿº ñîáîþ ãëîáàëüíó ³ñòîð³þ äîáóòêó òðàíçèö³éíèõ ñèñòåì òîä³
é ò³ëüêè òîä³, êîëè âîíà º äîïóñòèìîþ ïîñë³äîâí³ñòþ ñïðàöüîâóâàíü ïåðåõîä³â
ó ÌÏ. ³äïîâ³äíî åëåìåíòè ìíîæèíè Ò ñòàþòü ïåðåõîäàìè ÌÏ, à ãëîáàëüí³ ñòà-
íè ÒÑ (íàá³ð ñòàí³â êîæíî¿ ç ÒÑ, ùî áåðóòü ó÷àñòü â ñèíõðîííîìó äîáóòêó äî
àáî ï³ñëÿ ãëîáàëüíîãî ïåðåõîäó) ñòàþòü ì³ñöÿìè îòðèìàíî¿ ìåðåæ³.
Ìåðåæ³ Ïåòð³ òà ³íø³ ìåðåæåâ³ ìîäåë³ äîö³ëüíî âèêîðèñòîâóâàòè äëÿ âè-
çíà÷åííÿ êîðåêòíîñò³ ìîäåë³ íà âèñîêîìó ð³âí³ àáñòðàêö³¿, áåç ïðèâ’ÿçóâàííÿ
äî ñåìàíòèêè ïîçíà÷îê ïåðåõîä³â, òîáòî äëÿ ïåðåâ³ðêè íàäëèøêîâîñò³ ñèñòå-
ìè, íàÿâíîñò³ äåäëîê³â òîùî. Ïðèêëàäàìè àíàë³çó ìîäåëåé çà äîïîìîãîþ ÌÏ
º ðîáîòè [1] (äîñë³äæåííÿ äåäëîê³â òà ïàñòîê) òà [2] (ñòðóêòóðíà æèâó÷³ñòü íà
îáìåæåí³ñòü).
ÂÈÊÎÐÈÑÒÀÍÍß ÀÂÒÎÌÀÒÍÈÕ ÌÎÄÅËÅÉ ÄËß ÂÅÐÈÔ²ÊÀÖ²¯ ÑÏÅÖÈÔ²ÊÀÖ²É
Âèêîðèñòàííÿ ëèøå ìåðåæ Ïåòð³ íå çàâæäè º äîñòàòí³ì: íàâ³òü ÿêùî ñèñòåìà
â³äïîâ³äຠâñ³ì êðèòåð³ÿì íàä³éíîñò³ íà âèñîêîìó ð³âí³ àáñòðàêö³¿, âîíà ìîæå íå
â³äïîâ³äàòè âëàñíå ôóíêö³îíàëüíèì âèìîãàì. Çàñòîñóâàííÿ àâòîìàòíèõ ìîäåëåé
òà ôîðìóë ë³í³éíî-òåìïîðàëüíî¿ ëîã³êè íàäຠçìîãó çíàéòè ôðàãìåíòè øëÿõ³â âè-
198 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 4
êîíàííÿ (ïðåô³êñè), ùî ìîæóòü âèâåñòè ñèñòåìó ³ç ãëîáàëüíîãî ñòàíó ñåìàíòè÷-
íî¿ êîðåêòíîñò³ (òîáòî ñèñòåìà ïåðåñòຠâ³äïîâ³äàòè ïåâíèì ³íâàð³àíòàì).
ßê âèäíî ç îçíà÷åííÿ 2, äëÿ äîâ³ëüíî¿ ÒÑ A S X R s AP L� ( , , , , , )0 ìíîæèíà
ôóíêö³é L s Si i: � íàäຠçìîãó âèçíà÷èòè ôîðìóëè ñåìàíòè÷íî êîðåêòíî¿ ðîáîòè
ñèñòåìè äëÿ êîæíîãî ïåðåõîäó òà â êîæíîìó ñòàí³. Ôîðìàë³çóºìî ïðîöåñ àíàë³çó
â³äïîâ³äíîñò³ ñèñòåìè ôîðìóëàì, ùî îïèñóþòü ôóíêö³îíàëüí³ âèìîãè.
Îçíà÷åííÿ 3. ϳäìíîæèíó P íàçèâàþòü ë³í³éíî-òåìïîðàëüíîþ (LT) ôîðìó-
ëîþ/õàðàêòåðèñòèêîþ íàä ìíîæèíîþ àòîìàðíèõ ïðîïîçèö³éíèõ ôîðìóë ÀÐ,
ÿêùî P B AP� ( ( ))* , ³ B AP( ) — áóëåàí ìíîæèíè ÀÐ.
Îçíà÷åííÿ 4. Íåõàé äàíî ÇÒÑ A S X R I AP L� ( , , , , , ) òà ïîñë³äîâí³ñòü ñòàí³â
� � s s sn0 1� . Òðàñîþ trace ( )� ñê³í÷åííî¿ ïîñë³äîâíîñò³ � íàçèâàþòü ñëîâî
L s L s L sn( ) ( ) ( )0 1 � . Îòæå, ìíîæèíà òðàñ — öå ìíîæèíà ñê³í÷åííèõ ñë³â íàä àë-
ôàâ³òîì ïðîïîçèö³éíèõ ôîðìóë B AP( ) òàêèõ, ÿê³ âèêîíóþòüñÿ ó ñòàíàõ ö³º¿
ïîñë³äîâíîñò³. Ïîçíà÷èìî trace Ï trace Ï( ) ( ) |� �{ }� � , trace s trace Path s( ) ( ( ))� ,
Traces A trace s
s I
( ) ( )�
�
� , äå Path s( ) — ìàêñèìàëüíèé ôðàãìåíò øëÿõó �, ùî ïî÷è-
íàºòüñÿ ç³ ñòàíó s. «Ïîãàíèìè» ïðåô³êñàìè L s L s L sn( ) ( ) ( )0 1 � áóäåìî íàçèâàòè
ïðåô³êñè, ÿê³ ïîðóøóþòü ³ñòèíí³ñòü L si( ), òîáòî ñëîâà òàêîãî âèãëÿäó:
� �p L s L sn1 0( ) ( )� ,
�
� �p L s L sn n( ) ( )0 � .
Çâ³äñè âèïëèâຠìîæëèâ³ñòü âèçíà÷åííÿ ðåãóëÿðíî¿ ìîâè «ïîãàíèõ»
ïðåô³êñ³â BadPref A Traces A p
i
i( ) ( ( ))� �
�
�
�
� . Òàêà ìîâà àêöåïòóºòüñÿ ñê³í÷åí-
íèì àâòîìàòîì B Q AP f Q F� ( , , , , )0 , äå Q F0 � � � (ðèñ. 1).
ßêùî PA — âëàñòèâ³ñòü, âèêîíàííÿ ÿêî¿ ãàðàíòóº ïðàâèëüí³ñòü ôóíêö³îíó-
âàííÿ ÇÒÑ À , òîä³ ñåìàíòè÷íà êîðåêòí³ñòü ÇÒÑ À âèçíà÷àºòüñÿ óìîâîþ
Traces A BadPref P Traces A L BA( ) ( ) ( ) ( )� � � � �,
äå L B( ) — ìîâà, ÿêó àêöåïòóº àâòîìàò Â. Îòæå, àëãîðèòì ïåðåâ³ðêè
ë³í³éíî-òåìïîðàëüíî¿ ôîðìóëè P ì³ñòèòü òàê³ êðîêè.
1. Ñòâîðèòè àâòîìàò Áþõ³ [9], ùî àêöåïòóº ñëîâà, ÿê³ çàïåðå÷óþòü P.
2. Ïîáóäóâàòè äîáóòîê àâòîìàòà ³ ÇÒÑ, ùî ìîäåëþº âèõ³äíó ñèñòåìó.
3. Çíàéòè ïåðåð³ç øëÿõ³â, ÿê³ ãåíåðóº ÇÒÑ, ³ øëÿõ³â, ÿê³ àêöåïòóº àâòîìàò
(òàê çâàíèõ «ïîãàíèõ ïðåô³êñ³â»). ßêùî ïåðåð³ç º ïóñòîþ ìíîæèíîþ, ôîðìóëà Ð
º ³ñòèííîþ. ²íàêøå áóëî çíàéäåíî êîíòðïðèêëàä, ÿêèé äîâîäèòü íåâèêîíàííÿ
ôîðìóëè P.
Ðîçãëÿíåìî ïðîöåñ âèêîðèñòàííÿ àâòîìàòíèõ ìîäåëåé äëÿ àíàë³çó ñåìàíòè÷-
íî¿ êîðåêòíîñò³ ÇÒÑ, ùî îïèñóº ìîäåëü
âèêîíàííÿ çàñòîñóíêó â àðõ³òåêòóð³
NVIDIA CUDA (äåòàë³ ôîðìóâàííÿ ÇÒÑ
îïèñàíî â [2]). Çîáðàæåííÿ ÇÒÑ
Z S T R s AP L� ( , , , , , )1 íàâåäåíî íà
ðèñ. 2. Öÿ ñèñòåìà â³äïîâ³äຠêðèòåð³ÿì
íàä³éíîñò³ íà âèñîêîìó ð³âí³ àáñòðàêö³¿
(¿¿ âåðèô³êîâàíî çà äîïîìîãîþ ìåðåæå-
âèõ ìîäåëåé ó [1, 9]).
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 4 199
q0 q*
trase(s1),
…,
trase(sn)
p1,…, pn� �
Ðèñ. 1. Àâòîìàò Â, ÿêèé àêöåïòóº «ïîãàí³»
ïðåô³êñè, q Q0 0� , q F0 � , q F* �
Ó ÇÒÑ Z ³ñíóþòü òàê³ øëÿõè âèêîíàííÿ:
�1 1 2 3 4 7 8 1� s s s s s s s ,
� 2 1 2 5 6 7 8 1� s s s s s s s .
Òðàñè, ùî â³äïîâ³äàþòü øëÿõàì âèêîíàííÿ � i , º òàêèìè:
p trace L s L s L s L s L s L s L s1 1 1 2 3 4 7 8 1� �( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )� ,
p trace L s L s L s L s L s L s L s2 2 1 2 5 6 7 8 1� �( ) ( ) ( ) ( ) ( ) ( ) ( ) ( )� ,
Traces Z trace trace( ) ( ) ( )� � �� �1 2
� �L s L s L s L s L s L s L s L s( ) ( )( ( ) ( ) ( ) ( )) ( ) ( )1 2 3 4 5 6 7 8 .
Îäí³ºþ ç õàðàêòåðèñòèê, ÿê³ âèçíà÷àþòü ñåìàíòè÷íó êîðåêòí³ñòü ðîáîòè ñèñ-
òåìè, º âëàñòèâ³ñòü âçàºìíîãî âèêëþ÷åííÿ: ó ìåæàõ îäíîãî âàðïà â áóäü-ÿêèé
ìîìåíò ÷àñó ³íñòðóêö³ÿ ìîæå áóòè àáî àðèôìåòè÷íîþ, àáî ³íñòðóêö³ºþ äîñòóïó
äî ïàì’ÿò³ (àáî ³íñòðóêö³ÿ â³äñóòíÿ âçàãàë³). Öþ âëàñòèâ³ñòü ïðåäñòàâëåíî ó âè-
ãëÿä³ ë³í³éíî-òåìïîðàëüíî¿ ôîðìóëè P G f f� �( )ar mem , äå f ar — ïðîïîçèö³éíà
ôîðìóëà, ÿêà âêàçóº íà àðèôìåòè÷íèé òèï ³íñòðóêö³¿; f mem — ôîðìóëà, ùî âêà-
çóº íà òèï ³íñòðóêö³¿ äîñòóïó äî ïàì’ÿò³; G — ðîçøèðåííÿ áóëåâî¿ àëãåáðè ñå-
ìàíòèêîþ LT ëîã³êè, ùî îçíà÷ຠ«çàâæäè» [9].
Ïåðåâ³ðèìî ôîðìóëó Ð íà ³ñòèíí³ñòü, âèêîðèñòîâóþ÷è àëãîðèòì, íàâåäåíèé
âèùå. Àâòîìàò, ÿêèé àêöåïòóº ñëîâà, ùî çàïåðå÷óþòü ôîðìóëó Ð, ìຠâèãëÿä,
çîáðàæåíèé íà ðèñ. 3.
Ùîá ïåðåâ³ðèòè ³ñòèíí³ñòü ôîðìóëè Ð, íåîáõ³äíî îïèñàòè äîáóòîê ÇÒÑ Z òà BP ,
â ÿêîìó ïîòð³áíî ïåðåâ³ðèòè íàÿâí³ñòü øëÿõó-öèêëó òàêîãî, ùî º äîñòóïíèì ³ç ïî÷àò-
êîâîãî ñòàíó, òà ÿêèé âêëþ÷ຠâ ñåáå ñòàí ³ç F .
Øëÿõè, ùî çàäîâîëüíÿþòü çàçíà÷åí³ âèùå ïðàâèëà, â³äñóòí³ â ñèñòåì³, çîá-
ðàæåí³é íà ðèñ. 4. Öå îçíà÷àº, ùî Traces Z BadPref P( ) ( )� � �, òîáòî ìîæíà
ñòâåðäæóâàòè, ùî ôîðìóëà Ð º ³ñòèííîþ.
200 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 4
s3
s8
s4
t3
t1
s1 s2
t5
t2
s5 s6
t6
t7
t4
t8t9
s7
Ðèñ. 2. Ñõåìàòè÷íå çîáðàæåííÿ ÇÒÑ Z
q0
q1
{ f ar , f mem}
{} , { f ar } , { f mem} , { f ar , f mem}{} , { f ar } , { f mem}
Ðèñ. 3. Àâòîìàò B Q AP f Q FP � ( , , , , )0 , ùî àêöåïòóº çàïåðå÷åííÿ Ð, q F0 � , q F1 �
ÂÈÑÍÎÂÊÈ
Ó ðîáîò³ çàïðîïîíîâàíî ìåòîäîëîã³þ ïðîºêòóâàííÿ çàñòîñóíê³â äëÿ ñèñòåì ³ç
ìàñîâèì ïàðàëåë³çìîì íà ïðèêëàä³ GPGPU-ñèñòåì. Ìåòîäîëîã³ÿ º îð³ºíòîâàíîþ
íà àëãîðèòì³÷íèé åòàï ïðîºêòóâàííÿ òà ì³ñòèòü äâà îñíîâí³ êðîêè: ñòâîðåííÿ
ñïåöèô³êàö³¿ ñèñòåìè òà ¿¿ âåðèô³êàö³ÿ ³ àíàë³ç. Òàêîæ çàïðîïîíîâàíî ³ îïèñàíî
âèêîðèñòàííÿ ÑÀÀ-Ì Ãëóøêîâà òà àïàðàòó ÒÑ äëÿ îòðèìàííÿ ôîðìàë³çîâàíî¿
ñïåöèô³êàö³¿ ïðîºêòîâàíî¿ ñèñòåìè. Ðîçãëÿíóòî àâòîìàòí³ òà ìåðåæåâ³ ìîäåë³
äëÿ çàñòîñóâàííÿ íà åòàï³ âåðèô³êàö³¿ òà àíàë³çó íà ïðèêëàä³ àâòîìàò³â, ùî àê-
öåïòóþòü «ïîãàí³» ïðåô³êñè, òà ìåðåæ Ïåòð³ â³äïîâ³äíî. Ïîêàçàíî, ùî ïåðåâà-
ãîþ ìîäåëåé, ñòâîðåíèõ çà äîïîìîãîþ àïàðàòó ÒÑ º ¿õíÿ êîíâåðòîâàí³ñòü â
³íø³ ôîðìàòè, ùî ï³äòðèìóþòü òåìïîðàëüíó ëîã³êó (çîêðåìà, ìåðåæ³ Ïåòð³).
Íàâåäåíî ïðèêëàä ïðåäñòàâëåííÿ âëàñòèâîñò³ âçàºìíîãî âèêëþ÷åííÿ â ìîäåë³
âèêîíàííÿ çàñòîñóíêó â àðõ³òåêòóð³ NVIDIA CUDA ÿê ë³í³éíî-òåìïîðàëüíî¿
ôîðìóëè òà ¿¿ äîñë³äæåííÿ çà äîïîìîãîþ àâòîìàòíèõ ìîäåëåé.
ÑÏÈÑÎÊ Ë²ÒÅÐÀÒÓÐÈ
1. Ïîãîð³ëèé Ñ.Ä., Êðèâèé Ñ.Ë., Ñëèíüêî Ì.Ñ. Ïðîåêòóâàííÿ òà ìîäåëüíå îáãðóíòóâàííÿ çàñòîñóâàíü íà
îñíîâ³ â³äåîàäàïòåð³â. Óïðàâëÿþùèå ñèñòåìû è ìàøèíû. 2018. ¹ 4. Ñ. 46–56. https://doi.org/
10.15407/usim.2018.04.0046.
2. Kryvyi S., Porogilyy S., Slynko M. Transition systems as method of designing applications in GPGPU
technology. Problems in Programming. 2018. N 2–3. P. 12–20.
3. Anisimov A.V., Pogorilyy S.D., Vitel D.Yu. About the issue of algorithms formalized design for parallel
computer architectures. Applied and Computational Mathematics. 2013. Vol. 12, N 2. P. 140–151.
4. Ïîãîð³ëèé Ñ.Ä., Ìàð’ÿíîâñüêèé Â.À., Áîéêî Þ.Â., Âåðåùèíñüêèé Î.À. Äîñë³äæåííÿ ïàðàëåëüíèõ
ñõåì àëãîðèòìó Äàíöèãà äëÿ îá÷èñëþâàëüíèõ ñèñòåì ç³ ñï³ëüíîþ ïàì’ÿòòþ. Ìàòåìàòè÷í³ ìàøèíè
³ ñèñòåìè. 2009. ¹ 4. C. 27–37.
5. Pogorilyy S.D., Slynko M.S. Research and development of Johnson’s algorithm parallel schemes in GPGPU
technology. Problems in Programming. 2016. N 2–3. P. 105–112.
6. Pogorilyy S.D., Shkulipa I.Yu. A conception for creating a system of parametric design of parallel
algorithms and their software implementations. Cybernetics and Systems Analysis. 2009. Vol. 45, N 6.
P. 952–958.
7. Dijkstra E.W., Buxton J.N., Randell B. Software engineering techniques. Report on a Conference Sponsored
by the NATO Science Committee. (27–31 October 1969, Rome, Italy). Rome, Italy, 1969. P. 16.
ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 4 201
s8 , q0
{}
{}
s4 , q0s3 , q0
s2 , q0s1 , q0
s5 , q0 s6 , q0
s7 , q0
{}
s2 , q1
s3 , q1 s4 , q1
s5 , q1 s6 , q1
{ f ar , f mem }
{ f ar , f mem }
{ f ar }
{ f ar , f mem }
{ f ar } { f ar }
{ f mem }
{ f mem }
{ f mem }
{ f ar , f mem } { f ar , f mem }
Ðèñ. 4. Äîáóòîê àâòîìàòà BP ³ ÇÒÑ Z
8. Áîéêî Þ.Â., Êðèâèé Ñ.Ë., Ïîãîð³ëèé Ñ.Ä. òà ³í. Ìåòîäè òà íîâ³òí³ ï³äõîäè äî ïðîåêòóâàííÿ,
óïðàâë³ííÿ ³ çàñòîñóâàííÿ âèñîêîïðîäóêòèâíèõ ²Ò-³íôðàñòðóêòóð. Êè¿â: ÂÏÖ «Êè¿âñüêèé óí³âåðñè-
òåò», 2016. 447 ñ.
9. Albert E., Lanese I. Formal techniques for distributed objects, components, and systems. Proc. 36th IFIP
WG 6.1 International Conference, FORTE 2016, held as Part of the 11th International Federated
Conference on Distributed Computing Techniques, DisCoTec 2016, (June 6–9, 2016, Heraklion, Crete,
Greece). Heraklion, Crete, Greece, 2016. 275 p.
Íàä³éøëà äî ðåäàêö³¿ 20.02.2020
Ñ.Ä. Ïîãîðåëûé, Ì.Ñ. Ñëèíüêî
ÌÅÒÎÄÛ ÌÎÄÅËÈÐÎÂÀÍÈß È ÂÅÐÈÔÈÊÀÖÈÈ ÄËß ÏÐÎÅÊÒÈÐÎÂÀÍÈß
ÏÐÈËÎÆÅÍÈÉ Â ÃÅÒÅÐÎÃÅÍÍÛÕ ÀÐÕ²ÒÅÊÒÓÐÀÕ
Àííîòàöèÿ. Ïðåäëîæåíà ìåòîäîëîãèÿ ïðîåêòèðîâàíèÿ ïðèëîæåíèé äëÿ ñèñ-
òåì ñ ìàññîâûì ïàðàëëåëèçìîì íà ïðèìåðå GPGPU-ñèñòåì, îðèåíòèðîâàí-
íàÿ íà àëãîðèòìè÷åñêèé ýòàï ïðîåêòèðîâàíèÿ. Ðàññìîòðåíû äâå ôàçû ïðîåê-
òèðîâàíèÿ: ñîçäàíèå ôîðìàëüíîé ñïåöèôèêàöèè è åå èññëåäîâàíèå è âåðè-
ôèêàöèÿ. Äëÿ ïåðâîãî ýòàïà ïðåäëîæåíî èñïîëüçîâàíèå ìàòåìàòè÷åñêèõ
àïïàðàòîâ ñèñòåìû àëãîðèòìè÷åñêèõ àëãåáð/ìîäèôèöèðîâàííîé ñèñòåìû àë-
ãîðèòìè÷åñêèõ àëãåáð è òðàíçèöèîííûõ ñèñòåì. Äëÿ âòîðîãî ýòàïà ïðîàíà-
ëèçèðîâàíî èñïîëüçîâàíèå ñåòåâûõ è àâòîìàòíûõ ìîäåëåé è ïðèâåäåíû ïðå-
èìóùåñòâà êàæäîé èç íèõ.  ÷àñòíîñòè, ïðîâåäåíî èññëåäîâàíèå ìîäåëè
âû÷èñëåíèé â àðõèòåêòóðå NVIDIA CUDA ïðè ïîìîùè ñåòåé Ïåòðè, à òàê-
æå ôîðìóë ëèíåéíî-òåìïîðàëüíîé ëîãèêè è àâòîìàòíûõ ìîäåëåé.
Êëþ÷åâûå ñëîâà: òðàíçèöèîííûå ñèñòåìû, ñèñòåìû àëãîðèòìè÷åñêèõ àë-
ãåáð, GPGPU-ñèñòåìû, ñåòè Ïåòðè.
S. Pogorilyy, M. Slynko
MODELING AND VERIFICATION METHODS FOR APPLICATION DESIGN
IN HETEROGENEOUS ARCHITECTURES
Abstract. An application design methodology for massively parallelized systems
(GPGPU systems) focused on the algorithmic design phase is proposed. Two
design sub-steps are considered: creation of the formal specification of the
system; and its research and verification. The use of mathematical apparatuses
SAA/SAA-M as well as transition systems is proposed for the first step.
Advantages and specifics of using network and automaton models for the second
step are given. NVIDIA CUDA architecture computation model analysis is
proposed using Petri nets (network model) and using linear-temporal logic
formulas and Buchi automaton (automaton model).
Keywords: transition systems, systems of algorithmic algebras, GPGPU-systems,
Petri nets.
Ïîãîð³ëèé Ñåðã³é Äåì’ÿíîâè÷,
äîêòîð òåõí. íàóê, ïðîôåñîð, çàâ³äóâà÷ êàôåäðè Êè¿âñüêîãî íàö³îíàëüíîãî óí³âåðñèòåòó ³ìåí³ Òàðàñà
Øåâ÷åíêà, e-mail: sdp@univ.net.ua.
Ñëèíüêî Ìàêñèì Ñåðã³éîâè÷,
àñï³ðàíò Êè¿âñüêîãî íàö³îíàëüíîãî óí³âåðñèòåòó ³ìåí³ Òàðàñà Øåâ÷åíêà, e-mail: maxim.slinko@gmail.com.
202 ISSN 1019-5262. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2020, òîì 56, ¹ 4
|