Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах
Запропоновано методологію проєктування застосунків для систем із масовим паралелізмом на прикладі GPGPU-систем, орієнтовану на алгоритмічний етап проєктування. Розглянуто два етапи проєктування: створення формальної специфікації та її дослідження і верифікація. Для першого етапу запропоновано викори...
Saved in:
| Published in: | Кибернетика и системный анализ |
|---|---|
| Date: | 2020 |
| Main Authors: | , |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2020
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/190444 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах / С.Д. Погорілий, М.С. Слинько // Кибернетика и системный анализ. — 2020. — Т. 56, № 4. — С. 196–202. — Бібліогр.: 9 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1862555395537502208 |
|---|---|
| author | Погорілий, С.Д. Слинько, М.С. |
| author_facet | Погорілий, С.Д. Слинько, М.С. |
| citation_txt | Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах / С.Д. Погорілий, М.С. Слинько // Кибернетика и системный анализ. — 2020. — Т. 56, № 4. — С. 196–202. — Бібліогр.: 9 назв. — укр. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| 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).
|
| first_indexed | 2025-11-25T22:29:34Z |
| format | Article |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-190444 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1019-5262 |
| language | Ukrainian |
| last_indexed | 2025-11-25T22:29:34Z |
| publishDate | 2020 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| 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 |
| spellingShingle | Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах Погорілий, С.Д. Слинько, М.С. Нові засоби кібернетики, інформатики, обчислювальної техніки та системного аналізу |
| title | Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| title_alt | Методы моделирования и верификации для проектирования приложений в гетерогенных архітектурах Modeling and verification methods for application design in heterogeneous architectures |
| title_full | Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| title_fullStr | Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| title_full_unstemmed | Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| title_short | Методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| title_sort | методи моделювання і верифікації для проєктування застосунків у гетерогенних архітектурах |
| topic | Нові засоби кібернетики, інформатики, обчислювальної техніки та системного аналізу |
| topic_facet | Нові засоби кібернетики, інформатики, обчислювальної техніки та системного аналізу |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/190444 |
| 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 |