Peterson’s Algorithm total correctness proof in IPCL

Peterson’s Algorithm total correctness proof in IPCL

Доведено тотальну коректність алгоритму Пітерсона. За програмою зафіксовано стани та переходи транзиційної системи. Середо-вище виконання – паралельне з почерговим переключенням зі спільною пам’яттю. Сформульовано інваріант. Судження проведено в рамках методу доведення властивостей програм в Interle...

Ausführliche Beschreibung

Gespeichert in:
Bibliographische Detailangaben
Veröffentlicht in:Проблеми програмування
Datum:2016
1. Verfasser: Zhygallo, A.A.
Format: Artikel
Sprache:English
Veröffentlicht: Інститут програмних систем НАН України 2016
Schlagworte:
Паралельне програмування. Розподілені системи і мережі
Online Zugang:https://nasplib.isofts.kiev.ua/handle/123456789/126396
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Zitieren:Peterson’s Algorithm total correctness proof in IPCL / A.A. Zhygallo // Проблеми програмування. — 2016. — № 2-3. — С. 113-118. — Бібліогр.: 12 назв. — англ.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id nasplib_isofts_kiev_ua-123456789-126396
record_format dspace
spelling Zhygallo, A.A.
2017-11-23T13:04:30Z
2017-11-23T13:04:30Z
2016
Peterson’s Algorithm total correctness proof in IPCL / A.A. Zhygallo // Проблеми програмування. — 2016. — № 2-3. — С. 113-118. — Бібліогр.: 12 назв. — англ.
1727-4907
https://nasplib.isofts.kiev.ua/handle/123456789/126396
004.415.52, 681.3
Доведено тотальну коректність алгоритму Пітерсона. За програмою зафіксовано стани та переходи транзиційної системи. Середо-вище виконання – паралельне з почерговим переключенням зі спільною пам’яттю. Сформульовано інваріант. Судження проведено в рамках методу доведення властивостей програм в Interleaving Parallel Compositional Languages (IPCL). Спираючись на дану та інші роботи автора зроблено висновки щодо адекватності застосування методу для подібних задач завдяки гнучкості композиційно-номінативної платформи та його практичності і легкості застосування для реальних систем.
Доказана тотальная корректность алгоритма Петерсона. За программой зафиксированы состояния и переходы транзиционной системы. Среда выполнения – параллельная с поочередным переключением с общей памятью. Сформулировано инвариант. Суждение происходит в рамках метода доказательства свойств программ в Interleaving Parallel Compositional Languages (IPCL). Руководствуясь этой и другими работами автора сделано вывод об адекватности использования метода для подобных задач исходя из гибкости композиционно-номинативной платформы и его практичности и легкости в использовании для реальных систем.
The total correctness of the Peterson’s Algorithm has been proved. States and transitions were fixed by the program. Runtime environment considered is interleaving concurrency with shared memory. Invariant of the program was constructed. All reasoning provided in terms of Method for software properties proof in Interleaving Parallel Compositional Languages (IPCL). Conclusions about adequacy of the Method usage for such a kind of tasks (thanks to flexibility of composition-nominative platform) and its practicality as well as ease of use for real-world systems have been made based on this and other author’s works.
en
Інститут програмних систем НАН України
Проблеми програмування
Паралельне програмування. Розподілені системи і мережі
Peterson’s Algorithm total correctness proof in IPCL
Тотальна коректність алгоритму Петерсона в IPCL
Тотальная корректность алгоритма Петерсона в IPCL
Article
published earlier
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
title Peterson’s Algorithm total correctness proof in IPCL
spellingShingle Peterson’s Algorithm total correctness proof in IPCL
Zhygallo, A.A.
Паралельне програмування. Розподілені системи і мережі
title_short Peterson’s Algorithm total correctness proof in IPCL
title_full Peterson’s Algorithm total correctness proof in IPCL
title_fullStr Peterson’s Algorithm total correctness proof in IPCL
title_full_unstemmed Peterson’s Algorithm total correctness proof in IPCL
title_sort peterson’s algorithm total correctness proof in ipcl
author Zhygallo, A.A.
author_facet Zhygallo, A.A.
topic Паралельне програмування. Розподілені системи і мережі
topic_facet Паралельне програмування. Розподілені системи і мережі
publishDate 2016
language English
container_title Проблеми програмування
publisher Інститут програмних систем НАН України
format Article
title_alt Тотальна коректність алгоритму Петерсона в IPCL
Тотальная корректность алгоритма Петерсона в IPCL
description Доведено тотальну коректність алгоритму Пітерсона. За програмою зафіксовано стани та переходи транзиційної системи. Середо-вище виконання – паралельне з почерговим переключенням зі спільною пам’яттю. Сформульовано інваріант. Судження проведено в рамках методу доведення властивостей програм в Interleaving Parallel Compositional Languages (IPCL). Спираючись на дану та інші роботи автора зроблено висновки щодо адекватності застосування методу для подібних задач завдяки гнучкості композиційно-номінативної платформи та його практичності і легкості застосування для реальних систем. Доказана тотальная корректность алгоритма Петерсона. За программой зафиксированы состояния и переходы транзиционной системы. Среда выполнения – параллельная с поочередным переключением с общей памятью. Сформулировано инвариант. Суждение происходит в рамках метода доказательства свойств программ в Interleaving Parallel Compositional Languages (IPCL). Руководствуясь этой и другими работами автора сделано вывод об адекватности использования метода для подобных задач исходя из гибкости композиционно-номинативной платформы и его практичности и легкости в использовании для реальных систем. The total correctness of the Peterson’s Algorithm has been proved. States and transitions were fixed by the program. Runtime environment considered is interleaving concurrency with shared memory. Invariant of the program was constructed. All reasoning provided in terms of Method for software properties proof in Interleaving Parallel Compositional Languages (IPCL). Conclusions about adequacy of the Method usage for such a kind of tasks (thanks to flexibility of composition-nominative platform) and its practicality as well as ease of use for real-world systems have been made based on this and other author’s works.
issn 1727-4907
url https://nasplib.isofts.kiev.ua/handle/123456789/126396
citation_txt Peterson’s Algorithm total correctness proof in IPCL / A.A. Zhygallo // Проблеми програмування. — 2016. — № 2-3. — С. 113-118. — Бібліогр.: 12 назв. — англ.
work_keys_str_mv AT zhygalloaa petersonsalgorithmtotalcorrectnessproofinipcl
AT zhygalloaa totalʹnakorektnístʹalgoritmupetersonavipcl
AT zhygalloaa totalʹnaâkorrektnostʹalgoritmapetersonavipcl
first_indexed 2025-11-27T23:57:06Z
last_indexed 2025-11-27T23:57:06Z
_version_ 1850853015363256320

Ähnliche Einträge