Доведення властивості коректної роботи банківської системи виплати грошових переказів
Застосовано метод доведення властивостей паралельних програм, що виконуються багатоекземплярно в режимі почергового покрокового переключення і взаємодіють через спільну пам’ять, для доведення властивості коректності банківської системи виплати грошових переказів. В роботі поставлено задачу, побудова...
Saved in:
| Published in: | Проблеми програмування |
|---|---|
| Date: | 2016 |
| Main Authors: | , , , |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
Інститут програмних систем НАН України
2016
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/126397 |
| 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: | Доведення властивості коректної роботи банківської системи виплати грошових переказів / Ю.А. Остаповська, Т.В. Панченко, Н.В. Поліщук, М.О. Картавов // Проблеми програмування. — 2016. — № 2-3. — С. 119-132. — Бібліогр.: 10 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1862673476709515264 |
|---|---|
| author | Остаповська, Ю.А. Панченко, Т.В. Поліщук, Н.В. Картавов, М.О. |
| author_facet | Остаповська, Ю.А. Панченко, Т.В. Поліщук, Н.В. Картавов, М.О. |
| citation_txt | Доведення властивості коректної роботи банківської системи виплати грошових переказів / Ю.А. Остаповська, Т.В. Панченко, Н.В. Поліщук, М.О. Картавов // Проблеми програмування. — 2016. — № 2-3. — С. 119-132. — Бібліогр.: 10 назв. — укр. |
| collection | DSpace DC |
| container_title | Проблеми програмування |
| description | Застосовано метод доведення властивостей паралельних програм, що виконуються багатоекземплярно в режимі почергового покрокового переключення і взаємодіють через спільну пам’ять, для доведення властивості коректності банківської системи виплати грошових переказів. В роботі поставлено задачу, побудовано транзиційну систему для моделі зі спрощеним станом, сформульовано інваріант програми та проведено доведення істинності інваріанту над програмною системою у довільний момент часу. Зроблено висновки щодо зручності та адекватності застосування методу для доведення коректності паралельних систем.
Применен метод доказательства свойств параллельных программ, которые выполняются многоэкземплярно в режиме поочередного пошагового переключения и взаимодействуют через общую память, для доказательства свойства корректности банковской системы выплаты денежных переводов. В работе поставлена задача, построена транзиционная система для модели с упрощенным состоянием, сформулирован инвариант программы и проведено доказательство истинности инварианта над программной системой в любой момент времени. Сделаны выводы о удобстве и адекватности применения метода для доказательства корректности параллельных систем.
The method for properties proof for parallel programs running multiple-instance interleaving with shared memory was applied in order to prove the correctness property of the banking system for remittances payments. The task was stated, transitional system was built for the model with simplified state, and the program invariant was formulated and proved to keep true over the software system at any given time in this work. Conclusions about the convenience and adequacy of method application to prove the correctness of parallel systems were made.
|
| first_indexed | 2025-12-07T15:38:48Z |
| format | Article |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-126397 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Ukrainian |
| last_indexed | 2025-12-07T15:38:48Z |
| publishDate | 2016 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Остаповська, Ю.А. Панченко, Т.В. Поліщук, Н.В. Картавов, М.О. 2017-11-23T13:11:02Z 2017-11-23T13:11:02Z 2016 Доведення властивості коректної роботи банківської системи виплати грошових переказів / Ю.А. Остаповська, Т.В. Панченко, Н.В. Поліщук, М.О. Картавов // Проблеми програмування. — 2016. — № 2-3. — С. 119-132. — Бібліогр.: 10 назв. — укр. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/126397 004.415.52, 681.3 Застосовано метод доведення властивостей паралельних програм, що виконуються багатоекземплярно в режимі почергового покрокового переключення і взаємодіють через спільну пам’ять, для доведення властивості коректності банківської системи виплати грошових переказів. В роботі поставлено задачу, побудовано транзиційну систему для моделі зі спрощеним станом, сформульовано інваріант програми та проведено доведення істинності інваріанту над програмною системою у довільний момент часу. Зроблено висновки щодо зручності та адекватності застосування методу для доведення коректності паралельних систем. Применен метод доказательства свойств параллельных программ, которые выполняются многоэкземплярно в режиме поочередного пошагового переключения и взаимодействуют через общую память, для доказательства свойства корректности банковской системы выплаты денежных переводов. В работе поставлена задача, построена транзиционная система для модели с упрощенным состоянием, сформулирован инвариант программы и проведено доказательство истинности инварианта над программной системой в любой момент времени. Сделаны выводы о удобстве и адекватности применения метода для доказательства корректности параллельных систем. The method for properties proof for parallel programs running multiple-instance interleaving with shared memory was applied in order to prove the correctness property of the banking system for remittances payments. The task was stated, transitional system was built for the model with simplified state, and the program invariant was formulated and proved to keep true over the software system at any given time in this work. Conclusions about the convenience and adequacy of method application to prove the correctness of parallel systems were made. uk Інститут програмних систем НАН України Проблеми програмування Паралельне програмування. Розподілені системи і мережі Доведення властивості коректної роботи банківської системи виплати грошових переказів Доказательство свойства корректной работы банковской системы выплаты денежных переводов Correctness Property Proof for the Banking System for Money Transfer Payments Article published earlier |
| spellingShingle | Доведення властивості коректної роботи банківської системи виплати грошових переказів Остаповська, Ю.А. Панченко, Т.В. Поліщук, Н.В. Картавов, М.О. Паралельне програмування. Розподілені системи і мережі |
| title | Доведення властивості коректної роботи банківської системи виплати грошових переказів |
| title_alt | Доказательство свойства корректной работы банковской системы выплаты денежных переводов Correctness Property Proof for the Banking System for Money Transfer Payments |
| title_full | Доведення властивості коректної роботи банківської системи виплати грошових переказів |
| title_fullStr | Доведення властивості коректної роботи банківської системи виплати грошових переказів |
| title_full_unstemmed | Доведення властивості коректної роботи банківської системи виплати грошових переказів |
| title_short | Доведення властивості коректної роботи банківської системи виплати грошових переказів |
| title_sort | доведення властивості коректної роботи банківської системи виплати грошових переказів |
| topic | Паралельне програмування. Розподілені системи і мережі |
| topic_facet | Паралельне програмування. Розподілені системи і мережі |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/126397 |
| work_keys_str_mv | AT ostapovsʹkaûa dovedennâvlastivostíkorektnoírobotibankívsʹkoísistemiviplatigrošovihperekazív AT pančenkotv dovedennâvlastivostíkorektnoírobotibankívsʹkoísistemiviplatigrošovihperekazív AT políŝuknv dovedennâvlastivostíkorektnoírobotibankívsʹkoísistemiviplatigrošovihperekazív AT kartavovmo dovedennâvlastivostíkorektnoírobotibankívsʹkoísistemiviplatigrošovihperekazív AT ostapovsʹkaûa dokazatelʹstvosvoistvakorrektnoirabotybankovskoisistemyvyplatydenežnyhperevodov AT pančenkotv dokazatelʹstvosvoistvakorrektnoirabotybankovskoisistemyvyplatydenežnyhperevodov AT políŝuknv dokazatelʹstvosvoistvakorrektnoirabotybankovskoisistemyvyplatydenežnyhperevodov AT kartavovmo dokazatelʹstvosvoistvakorrektnoirabotybankovskoisistemyvyplatydenežnyhperevodov AT ostapovsʹkaûa correctnesspropertyproofforthebankingsystemformoneytransferpayments AT pančenkotv correctnesspropertyproofforthebankingsystemformoneytransferpayments AT políŝuknv correctnesspropertyproofforthebankingsystemformoneytransferpayments AT kartavovmo correctnesspropertyproofforthebankingsystemformoneytransferpayments |