Correctness Property Proof for the Banking System for Money Transfer Payments

Correctness Property Proof for the Banking System for Money Transfer Payments

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 stat...

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2018
Автори: Ostapovska, Yu.A., Panchenko, T.V., Polishchuk, N.V., Kartavov, M.O.
Формат: Стаття
Мова:Ukrainian
Опубліковано: Інститут програмних систем НАН України 2018
Теми:
software correctness
safety property proof
concurrent program
interleaving
invariant
IPCL
composition-nominative languages
formal verification
UDC 004.415.52
Онлайн доступ:https://pp.isofts.kiev.ua/index.php/ojs1/article/view/187
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Problems in programming
Завантажити файл: Pdf

Репозитарії

Problems in programming
id pp_isofts_kiev_ua-article-187
record_format ojs
resource_txt_mv ppisoftskievua/8b/9bd3c1d7018df44a369d0526f145aa8b.pdf
spelling pp_isofts_kiev_ua-article-1872024-04-28T13:09:57Z Correctness Property Proof for the Banking System for Money Transfer Payments Доказательство свойства корректной работы банковской системы выплаты денежных переводов Доведення властивості коректної роботи банківської системи виплати грошових переказів Ostapovska, Yu.A. Panchenko, T.V. Polishchuk, N.V. Kartavov, M.O. software correctness; safety property proof; concurrent program; interleaving; invariant; IPCL; composition-nominative languages; formal verification UDC 004.415.52 корректность программного обеспечения; доказательство частичной корректности; параллельная программа; interleaving; инвариант; IPCL; композиционно-номинативные языки; формальная верификация УДК 004.415.52 коректність програмного забезпечення; доведення часткової коректності; паралельна програма; interleaving; інваріант; IPCL; композиційно-номінативні мови; формальна верифікація УДК 004.415.52 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.Problems in programming 2016; 2-3: 119-132 Применен метод доказательства свойств параллельных программ, которые выполняются многоэкземплярно в режиме поочередного пошагового переключения и взаимодействуют через общую память, для доказательства свойства корректности банковской системы выплаты денежных переводов. В работе поставлена задача, построена транзиционная система для модели с упрощенным состоянием, сформулирован инвариант программы и проведено доказательство истинности инварианта над программной системой в любой момент времени. Сделаны выводы о удобстве и адекватности применения метода для доказательства корректности параллельных систем.Problems in programming 2016; 2-3: 119-132 Застосовано метод доведення властивостей паралельних програм, що виконуються багатоекземплярно в режимі почергового пок-рокового переключення і взаємодіють через спільну пам’ять, для доведення властивості коректності банківської системи виплати грошових переказів. В роботі поставлено задачу, побудовано транзиційну систему для моделі зі спрощеним станом, сформульовано інваріант програми та проведено доведення істинності інваріанту над програмною системою у довільний момент часу. Зроблено висновки щодо зручності та адекватності застосування методу для доведення коректності паралельних систем.Problems in programming 2016; 2-3: 119-132 Інститут програмних систем НАН України 2018-07-06 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/187 10.15407/pp2016.02-03.119 PROBLEMS IN PROGRAMMING; No 2-3 (2016); 119-132 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2016); 119-132 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2016); 119-132 1727-4907 10.15407/pp2016.02-03 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/187/182 Copyright (c) 2017 ПРОБЛЕМИ ПРОГРАМУВАННЯ
institution Problems in programming
baseUrl_str https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date 2024-04-28T13:09:57Z
collection OJS
language Ukrainian
topic software correctness
safety property proof
concurrent program
interleaving
invariant
IPCL
composition-nominative languages
formal verification
UDC 004.415.52
spellingShingle software correctness
safety property proof
concurrent program
interleaving
invariant
IPCL
composition-nominative languages
formal verification
UDC 004.415.52
Ostapovska, Yu.A.
Panchenko, T.V.
Polishchuk, N.V.
Kartavov, M.O.
Correctness Property Proof for the Banking System for Money Transfer Payments
topic_facet software correctness
safety property proof
concurrent program
interleaving
invariant
IPCL
composition-nominative languages
formal verification
UDC 004.415.52
корректность программного обеспечения
доказательство частичной корректности
параллельная программа
interleaving
инвариант
IPCL
композиционно-номинативные языки
формальная верификация
УДК 004.415.52
коректність програмного забезпечення
доведення часткової коректності
паралельна програма
interleaving
інваріант
IPCL
композиційно-номінативні мови
формальна верифікація
УДК 004.415.52
format Article
author Ostapovska, Yu.A.
Panchenko, T.V.
Polishchuk, N.V.
Kartavov, M.O.
author_facet Ostapovska, Yu.A.
Panchenko, T.V.
Polishchuk, N.V.
Kartavov, M.O.
author_sort Ostapovska, Yu.A.
title Correctness Property Proof for the Banking System for Money Transfer Payments
title_short Correctness Property Proof for the Banking System for Money Transfer Payments
title_full Correctness Property Proof for the Banking System for Money Transfer Payments
title_fullStr Correctness Property Proof for the Banking System for Money Transfer Payments
title_full_unstemmed Correctness Property Proof for the Banking System for Money Transfer Payments
title_sort correctness property proof for the banking system for money transfer payments
title_alt Доказательство свойства корректной работы банковской системы выплаты денежных переводов
Доведення властивості коректної роботи банківської системи виплати грошових переказів
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.Problems in programming 2016; 2-3: 119-132
publisher Інститут програмних систем НАН України
publishDate 2018
url https://pp.isofts.kiev.ua/index.php/ojs1/article/view/187
work_keys_str_mv AT ostapovskayua correctnesspropertyproofforthebankingsystemformoneytransferpayments
AT panchenkotv correctnesspropertyproofforthebankingsystemformoneytransferpayments
AT polishchuknv correctnesspropertyproofforthebankingsystemformoneytransferpayments
AT kartavovmo correctnesspropertyproofforthebankingsystemformoneytransferpayments
AT ostapovskayua dokazatelʹstvosvojstvakorrektnojrabotybankovskojsistemyvyplatydenežnyhperevodov
AT panchenkotv dokazatelʹstvosvojstvakorrektnojrabotybankovskojsistemyvyplatydenežnyhperevodov
AT polishchuknv dokazatelʹstvosvojstvakorrektnojrabotybankovskojsistemyvyplatydenežnyhperevodov
AT kartavovmo dokazatelʹstvosvojstvakorrektnojrabotybankovskojsistemyvyplatydenežnyhperevodov
AT ostapovskayua dovedennâvlastivostíkorektnoírobotibankívsʹkoísistemiviplatigrošovihperekazív
AT panchenkotv dovedennâvlastivostíkorektnoírobotibankívsʹkoísistemiviplatigrošovihperekazív
AT polishchuknv dovedennâvlastivostíkorektnoírobotibankívsʹkoísistemiviplatigrošovihperekazív
AT kartavovmo dovedennâvlastivostíkorektnoírobotibankívsʹkoísistemiviplatigrošovihperekazív
first_indexed 2024-09-25T04:02:50Z
last_indexed 2024-09-25T04:02:50Z
_version_ 1818527318869540864
fulltext Паралельне програмування. Розподілені системи і мережі © Ю.А. Остаповська, Т.В. Панченко, Н.В. Поліщук, М.О. Картавов, 2016 ISSN 1727-4907. Проблеми програмування. 2016. № 2–3. Спеціальний випуск 119 УДК 004.415.52, 681.3 ДОВЕДЕННЯ ВЛАСТИВОСТІ КОРЕКТНОЇ РОБОТИ БАНКІВСЬКОЇ СИСТЕМИ ВИПЛАТИ ГРОШОВИХ ПЕРЕКАЗІВ Ю.А. Остаповська, Т.В. Панченко, Н.В. Поліщук, М.О. Картавов Застосовано метод доведення властивостей паралельних програм, що виконуються багатоекземплярно в режимі почергового пок- рокового переключення і взаємодіють через спільну пам’ять, для доведення властивості коректності банківської системи виплати грошових переказів. В роботі поставлено задачу, побудовано транзиційну систему для моделі зі спрощеним станом, сформульовано інваріант програми та проведено доведення істинності інваріанту над програмною системою у довільний момент часу. Зроблено висновки щодо зручності та адекватності застосування методу для доведення коректності паралельних систем. Ключові слова: коректність програмного забезпечення, доведення часткової коректності, паралельна програма, interleaving, інварі- ант, IPCL, композиційно-номінативні мови, формальна верифікація Применен метод доказательства свойств параллельных программ, которые выполняются многоэкземплярно в режиме поочередного пошагового переключения и взаимодействуют через общую память, для доказательства свойства корректности банковской системы выплаты денежных переводов. В работе поставлена задача, построена транзиционная система для модели с упрощенным состояни- ем, сформулирован инвариант программы и проведено доказательство истинности инварианта над программной системой в любой момент времени. Сделаны выводы о удобстве и адекватности применения метода для доказательства корректности параллельных систем. Ключевые слова: корректность программного обеспечения, доказательство частичной корректности, параллельная программа, interleaving, инвариант, IPCL, композиционно-номинативные языки, формальная верификация 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. Key words: software correctness, safety property proof, concurrent program, interleaving, invariant, IPCL, composition-nominative lan- guages, formal verification Постановка задачі та аналіз. Формулювання властивості коректності системи Розглянемо застосування методики доведення властивостей паралельних програм у IPCL [1–3]. Задача стосується доведення критичних властивостей системи виплати міжнародних грошових переказів Vigo Remit- tance Corp., реалізованої в ВАТ “Державний ощадний банк України” (надалі – банк). Сформулюємо задачу. Для виплати певного переказу одержувачу здійснюється авторизація – отримання дозволу на виплату цього переказу даному одержувачу (точніше, в даному випадку – претенденту на одержан- ня). Така процедура виконується в середовищі SQL, модель роботи якого – паралелізм через спільну пам’ять в режимі почергового виконання, тобто кілька процедур виконуються “одночасно” в покроковому режимі, при- чому кожну дискрету часу виконується тільки одна команда тільки одного процесу (із усіх, запущених у пара- лель). Процедура авторизації передбачає аутентифікацію та ідентифікацію претендента на одержання грошей шляхом перевірки наданих ним даних у запиті стосовно грошового переказу. Якщо інформація надана правиль- но, тобто співпадає з наявною у базі даних (база даних поповнюється паралельно з пересиланням грошей при надходженні нових переказів для виплати), переказ не заблоковано (переказ блокується після кількох невдалих авторизацій або з інших особливих обставин – анулювання, тощо – та може бути розблокований спеціальним оператором системи) та не виплачено, одержувач є дійсно тим, за кого себе видає, то авторизація вважається пройденою успішно і надається дозвіл на виплату переказаних грошей оператором системи (працівником бан- ку) одержувачу. Ця процедура є необхідною (тобто попередній розподіл переказів по відділеннях банку є не- можливим), оскільки повинна забезпечуватись можливість одержувачу отримати призначений йому грошовий переказ (тобто переказ на своє ім’я) у будь-якій точці (в будь-якому відділенні банку) країни. Банку необхідно гарантувати, що система працює коректно, іншими словами, що він не втрачає кошти. Оскільки формалізувати ідентифікацію одержувача (людини) безглуздо (перевірка відповідності паспортних даних, порівняння по вклеєній у паспорт фотокартці, перевірка автентичності фотокартки, непідробленість пас- порту взагалі тощо), зосередимось на ідентифікації переказу та його стану і відповідних кроках процедури ав- торизації. З цих позицій питання коректності, фактично, зводиться до питання неможливості виплати зайвих коштів. Якщо врахувати, що авторизація передбачає, зокрема, перевірку суми переказу, то зрозуміло, що в ме- жах одного переказу банк не може втратити “зайвих” грошей. Звідси, банку потрібно гарантувати, фактично, що жодний переказ не може бути виплачений більше одного разу. (Певний переказ буде виплачений один раз лише за умови відповідності інформації в базі даних переказів з наданими претендентом на його одержання реквізитами.) Звідси, коректність системи зводиться до необхідності довести, що один і той самий переказ не може бу- ти виплачений двічі (і більше разів), тобто що дозвіл на його виплату (авторизація виплати) не може бути отри- маний двічі (і більше). Паралельне програмування. Розподілені системи і мережі 120 Проектування Тепер розглянемо детальніше процедуру авторизації. Легко побудувати більш-менш очевидну покрокову процедуру авторизації переказу в першому наближенні: 1) зафіксувати чергову спробу авторизації 2) якщо переказ не заблоковано то якщо переказ не виплачено то якщо надана коректна інформація по переказу то (*) якщо ця інформація співпадає з даними у базі то (*) авторизувати виплату переказу інакше (в усіх інших випадках) відмовити в авторизації 3) якщо спроб авторизації накопичилось більше 2, то заблокувати переказ. Опустимо з аналізу перевірку коректності інформації (помічено *), оскільки реально це не впливає суттє- во на результат авторизації (більш того, ці перевірки складають банківську таємницю) – так, це дуже важлива перевірка, але, як побачимо далі, вона не є критичною для доведення властивості, яка нас цікавить (іншими словами, цілком зрозуміло, як її робити). (Очевидно, що коли хоча б одна з умов не виконується, авторизація не пройде, оскільки вона відбувається лише у випадку, коли всі умови повертають True під час перевірки – при- наймні логічно так має бути.) Як було відзначено, середовище SQL є середовищем з паралелізмом із взаємодією через спільну пам’ять. В зв’язку з цим слід також зауважити, що якщо деяка умова повернула True під час об- числення її значення, то пізніше (при виконанні наступних кроків) вона (той самий предикат умовного операто- ру) може потенційно прийняти значення False, отже коли виконання дійде до блоку “then” з “if-then-else”, на- приклад, то значення предиката умови може вже бути False (хоча до виконання блоку “then” можна було прис- тупити лише в ситуації, коли при обчислення предикату умови було отримано результат True). А отже, ми мо- жемо отримати суперечливу ситуацію і зокрема, наприклад, авторизувати виплату одного переказу двічі. Не зосереджуючись докладно на архітектурних рішеннях та дизайні системи, відзначимо ключові думки та їх обґрунтування. 1. Вузьке місце. Інтуїтивно зрозуміло, що критичним місцем системи є паралельна спроба авторизації одного й того ж переказу кілька разів (наприклад, коли дехто перехопив коректну інформацію про переказ і намагається отримати авторизацію не будучи дійсним одержувачем переказу). Цей факт не впливає на подаль- шу побудову системи та доведення необхідної властивості, але дозволяє краще розуміти вузькі місця і прийма- ти правильні рішення щодо дизайну та архітектури системи. 2. Рівень ізоляції транзакцій SQL (Transaction Isolation Level). Кожна авторизація складає транзакцію (насправді – дві транзакції: фіксація намірів авторизації та результат авторизації – власне авторизація). Рі- вень ізоляції обирається Read Committed. Зрозуміло, що нам необхідний рівень, який гарантував би немож- ливість одночасної роботи з одним переказом (фактично, не допускав би інтерференцію процесів), але, по - перше, найсуворіший рівень ізоляції – Serializable – не еквівалентний послідовному виконанню процесів (то- ді була б гарантована свобода від інтерференції), а по-друге, рівень ізоляції Serializable рекомендований до застосування лише у випадках зі складною логікою обчислень (в даній системі логіка не є надто складною) і має великий відсоток відкатів транзакцій (transaction roll-back), що призводить до необхідності повторних спроб виконання транзакцій, ускладнення внутрішньої логіки виконання команд SQL-сервером (більше бло- кувань будуть утримуватись довший час) та зменшення загальної швидкодії системи (детальніше про це мо- жна прочитати в документації по будь-якому SQL-серверу – Microsoft SQL Server, PostgreSQL, а також в [4]). Звичайно, останнє є неприпустимим у випадку критичних до часу банківських систем. 3. Уточнення алгоритму авторизації. Введемо перевірку на кількість паралельних (виконуваних одночас- но) авторизацій. Це можливо, оскільки ми фіксуємо спробу авторизації в журналі, незалежно від її результату, який з’ясується пізніше. Таким чином, уточнений алгоритм авторизації виглядатиме наступним чином: 1) записати чергову спробу авторизації 2) якщо кількість одночасних (паралельних) спроб = 1, то якщо переказ не заблоковано то якщо переказ не виплачено то якщо надана коректна інформація по переказу і ця інформація співпадає з даними у базі то (*) авторизувати виплату переказу інакше (в усіх інших випадках) відмовити в авторизації 3) якщо спроб авторизації накопичилось більше 2, то заблокувати переказ. Паралельне програмування. Розподілені системи і мережі 121 Паралельно з цим спеціальний оператор по вирішенню конфліктів може розблокувати спірні перекази, тобто паралельно виконується процес: розблокувати переказ Побудова програми IPCL та моделюючої транзиційної системи Нам знадобиться модель системи (модель реальної системи на мові SQL в мові IPCL). Отже, одним з ключових моментів є визначення адекватного рівня деталізації системи (і, відповідно, доведення). Є різні можливості в даному аспекті – так, можна розглядати модель як в [5,6], тобто моделювати виконання опера- цій SQL-сервером (деталізувати до рівня операцій з таблицям), а можна абстрагуватись від представлення та роботи безпосередньо з даними – і розглядати функціонування системи на вищому рівні абстракції. Ми бу- демо покладатись на коректність реалізації SQL-сервера, а, отже, розглядати (точніше, використовувати) йо- го операції без деталізації щодо їх реалізації – тобто розглядатимемо коректність програми відносно SQL. Ще одне зауваження. В моделі ми зосередимось на роботі з одним переказом. Зрозуміло, що робота з рі- зними переказами, хоч і виконувана в паралель, не інтерферує (немає взаємного впливу процесів авторизації різних переказів один на інший, адже такими процесами зачіпаються рядки таблиць, перетин яких є порожнім – оскільки вони мають принаймні різні коди переказів). Тому ми явно не будемо вказувати ні номер переказу, ні інформацію щодо нього. Уточнення процедури авторизації. Нехай у нас є три таблиці: інформаційна (про перекази) Inf, автори- заційна (журнал авторизацій та спроб) Auth та таблиця з інформацією щодо блокувань Block. Авторизаційна таблиця містить кортежі зі станом спроб авторизації – “виплачено” (тобто авторизована виплата), “спроба авторизації” (зараз відбувається, in progress) та “відмова” (із зазначенням причини). Розглянемо ситуацію роботи з деяким переказом з кодом Invoice. Позначимо кількості рядків в цих таблицях наступним чином: A – кількість виплат переказу Invoice, тобто кількість рядків таблиці Auth, які відносяться до Invoice та мають статус “виплачено”, P – кількість паралельних (одночасних) спроб авторизації (виплати) переказу, тобто кількість рядків таб- лиці Auth, які відносяться до Invoice та мають статус “спроба авторизації”, T – накопичувальна кількість всіх спроб виплати переказу, тобто загальна кількість рядків таблиці Auth, які відносяться до Invoice, B – блокування переказу (0 = немає, 1 = є), тобто останній стан блокування Invoice, згідно таблиці Block, якщо такі записи є (1 – заблоковано або 0 – розблоковано), або 0, якщо немає відповідних записів в таблиці Block. Зрозуміло, що значення всіх змінних завжди є невід’ємними цілими числами (це – кількості рядків в таб- лицях, окрім B, що приймає значення 0 або 1). Тепер можна виписати процедуру авторизації у вигляді IPCL-програми над станом зі змінними A, P, T, B: Auth_Prog = (T, P) := (T +1, P +1); // фіксація спроби авторизації if ( P = 1 ) then if ( B = 0 ) then if ( A = 0 ) then if ( data_provided_correct() ) then (A, P) := (A +1, P –1) // фіксація успішної авторизації else P := P –1 // завершення авторизації відмовою else P := P –1 else P := P –1 else P := P –1; if ( T > 2 ) then B := 1 else Id; де data_provided_correct() – предикат, що повертає True, коли передані дані щодо переказу є коректними згідно бази даних переказів (таблиця Inf) та False у протилежному випадку. Паралельно може виконуватись процес “розблокувати переказ”: Unblock = B := 0; Семантика відповідних функцій алгебри IPCLA буде визначена природним чином: sem (T, P) := (T +1, P +1) (d)  d  [ T  (T(d) + 1), P  (P(d) + 1) ], sem P = 1 (d)  IF ( P(d) = 1, True, False ), Паралельне програмування. Розподілені системи і мережі 122 sem B = 0 (d)  IF ( B(d) = 0, True, False ), sem A = 0 (d)  IF ( A(d) = 0, True, False ), sem data_provided_correct() (d)  choice (True, False), sem (A, P) := (A +1, P –1) (d)  d  [ A  (A(d) + 1), P  (P(d) – 1) ], sem P := P –1 (d)  d  [ P  (P(d) – 1) ], sem T > 2 (d)  IF ( T(d) > 2, True, False ), sem B := 1 (d)  d  [ B  1 ], sem Id (d)  d (identity, дане не змінюється), sem B := 0 (d)  d  [ B  0 ], де choice (A, B) – недетермінований вибір між значеннями A та B. Дане d має загальний вигляд d = [ P p, T  t, A  a, B  b ]. Таким чином, маємо програму в IPCL (точніше, в підкласі – SeqILProgs): Program = Auth_Progn || Unblockm . Оскільки у нас немає локальних даних (точніше, для спрощення ми від них відмовились – зокрема, в data_provided_correct()), побудуємо спрощену модель (зі спрощеними станами) [7]. Після виконання алгоритму розстановки міток отримаємо: Auth_Prog = [M1:] (T, P) := (T +1, P +1); if [M2:] ( P = 1 ) then if [M3:] ( B = 0 ) then if [M4:] ( A = 0 ) then if [M5:] ( data_provided_correct() ) then [M6:] (A, P) := (A +1, P –1) else [M7:] P := P –1 else [M8:] P := P –1 else [M9:] P := P –1 else [M10:] P := P –1; if [M11:] ( T > 2 ) then [M12:] B := 1 else [M13:] Id; [M14:] Unblock = [M15:] B := 0; [M16:] Множина SStates буде представляти собою підмножину N16D, згідно спрощеного варіанту методу, де D = ND(V, W) – спільні глобальні дані для всіх процесів, причому {A, P, T, B}V та N{0}W. Функція SStep (виконання програми Program) буде визначена за цим алгоритмом наступним чином: { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1–1, s2+1, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, sem (T, P) := (T +1, P +1) (d)) ) | s1>0 & iN16  siN }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2–1, s3+1, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s2>0 & iN16  siN & sem P = 1 (d)=True }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2–1, s3, s4, s5, s6, s7, s8, s9, s10+1, s11, s12, s13, s14, s15, s16, d) ) | s2>0 & iN16  siN & sem P = 1 (d)=False }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3–1, s4+1, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s3>0 & iN16  siN & sem B = 0 (d)=True }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3–1, s4, s5, s6, s7, s8, s9+1, s10, s11, s12, s13, s14, s15, s16, d) ) | s3>0 & iN16  siN & sem B = 0 (d)=False }  Паралельне програмування. Розподілені системи і мережі 123 { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4–1, s5+1, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s4>0 & iN16  siN & sem A = 0 (d)=True }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4–1, s5, s6, s7, s8+1, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s4>0 & iN16  siN & sem A = 0 (d)=False }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5–1, s6+1, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s5>0 & iN16  siN & sem data_provided_correct() (d)=True }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5–1, s6, s7+1, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s5>0 & iN16  siN & sem data_provided_correct() (d)=False }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6–1, s7, s8, s9, s10, s11+1, s12, s13, s14, s15, s16, sem (A, P) := (A +1, P –1) (d)) ) | s6>0 & iN16  siN }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7–1, s8, s9, s10, s11+1, s12, s13, s14, s15, s16, sem P := P –1 (d)) ) | s7>0 & iN16  siN }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8–1, s9, s10, s11+1, s12, s13, s14, s15, s16, sem P := P –1 (d)) ) | s8>0 & iN16  siN }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9–1, s10, s11+1, s12, s13, s14, s15, s16, sem P := P –1 (d)) ) | s9>0 & iN16  siN }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10–1, s11+1, s12, s13, s14, s15, s16, sem P := P –1 (d)) ) | s10>0 & iN16  siN }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11–1, s12+1, s13, s14, s15, s16, d) ) | s11>0 & iN16  siN & sem T > 2 (d)=True }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11–1, s12, s13+1, s14, s15, s16, d) ) | s11>0 & iN16  siN & sem T > 2 (d)=False }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12–1, s13, s14+1, s15, s16, sem B := 1 (d)) ) | s12>0 & iN16  siN }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13–1, s14+1, s15, s16, sem Id (d)) ) | s13>0 & iN16  siN }  { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15–1, s16+1, sem B := 0 (d)) ) | s15>0 & iN16  siN }, де si – кількість процесів, що знаходяться в позиції (на мітці) [Mi:] в даний момент часу. Візьмемо SStartStates = { (n, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, m, 0, d) | nN, mN, [ P  0, T  0, A  0, B  0 ]  d } та SStopStates = { s | s=(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, n, 0, m, d’) & nN & mN & s1, s2, …, sl  (s1SStartStates & sl=s & (iNl-1  (si, si+1)SStep) ) }. В даній постановці модель можна розглядати як таку, що описує повний шлях існування (“життєвий цикл”) певного переказу (його спроби авторизації – вдалі та невдалі, блокування та розблокування спеціаль- ним оператором). Оскільки n та m (ступені підпрограм) можуть бути довільними цілими невід’ємними чис- лами, то, дійсно, модель задає довільний можливий шлях роботи з будь-яким одним переказом (іншими сло- вами, сімейство програм). Обробка різних переказів не перетинається – такі процеси обробки переказів не інтерферують. До речі, програма P, зокрема, може перетворитись на послідовне виконання її підпрограм (в довільному ступені), згідно заданої семантики мови IPCL та алгоритму побудови моделі – така ситуація, ма- буть, найчастіше виникає на практиці. Але разом з тим програма (і модель) передбачає можливість перетина- тись довільним чином операторам (окремим діям) паралельних процесів (згідно заданої семантики – та прин- ципів паралелізму з почерговим виконанням, interleaving concurrency). Отже, модель передбачає і описує всі можливі траси виконання програми Program та системи (авторизації виплати переказів), що моделюється. Паралельне програмування. Розподілені системи і мережі 124 Доведення коректності Таким чином, необхідно довести властивість A1, якщо на початку роботи A1, тобто {A1} Program {A1}. Якщо PreCond(S) = (A(d)1), PostCond(S) = (A(d)1), де S = (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), то необхідно показати, що SSStartStates  S’SStopStates  (PreCond(S) & (S, S’)SStep  PostCond(S)). Розглянемо Inv(S)  (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ), де S = (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d). Цей інваріант, насправді, досить легко утворити, розуміючи логіку програми та описані вище критичні місця. Так, він вказує, що кількість паралельних (конкуруючих) процесів, які намагаються безпосередньо авто- ризувати даний переказ, не може бути більше одного (s3+s4+s5+s61) – умова (P=1) відсікає інші можливості, при цьому значення A може бути лише 0 або 1. Якщо ж значення є вже 1 (переказ авторизовано і виплачено), то жоден процес не потрапить в “зону безпосередньої авторизації” ( (A(d)=1) & (s5=0) & (s6=0) ). Ще додається одна умова “цілісності” – оператори виконуються у відповідній послідовності, “фантомні” (нові по ходу вико- нання) програми (підпрограми авторизації) не виникають, а кількість програм в точках перевірки (s2, s3, s4, s5, s6, s7, s8, s9, s10) дорівнює кількості паралельних спроб авторизації даного переказу (P). Більш того, в інваріанті не фігурує змінна B, тобто блокування несуттєво впливають на хід авторизації (з точки зору інтерференції та пара- лелізму), що зрозуміло з логіки програми. (Отже, оператори, пов’язані з блокуванням, можна було б взагалі опустити з моделі та аналізу.) Згідно методики доведемо, що InvCond(Inv, PreCond, PostCond) = True, де InvCond(Inv, PreCond, PostCond) = SSStartStates  ( PreCond(S)  Inv(S) ) & SSStopStates  ( Inv(S)  PostCond(S) ) & (S, S’)SStep  ( Inv(S)  Inv(S’) ), а також перевіримо, що SSStartStates  PreCond(S). Тоді будемо мати SSStopStates  PostCond(S). Оскільки для кожного SSStartStates, де S = (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), маємо s2=s3=s4=s5=s6=s7=s8=s9=s10=0, P(d)=0 та A(d)=0  A(d)=1, що випливає з (A(d)1), тобто PreCond(S), то SSStartStates  ( PreCond(S)  Inv(S) ). Покажемо, що SSStates  ( Inv(S)  PostCond(S) ). Очевидно, { (A(d)=0)  A(d)1, (A(d)=1)  A(d)1  ( (A(d)=1) & (s5=0) & (s6=0) )  A(d)1 }  ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) )  A(d)1  (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) )  A(d)1 = Inv(S)  PostCond(S). Отже, зокрема, SSStopStates  ( Inv(S)  PostCond(S) ). Залишається довести, що (S, S’)SStep  ( Inv(S)  Inv(S’) ). Розглянемо всі пари (S, S’)SStep і покажемо, що для кожної такої пари спрощених станів якщо Inv(S), то і Inv(S’). Дослідимо множини пар станів (S, S’)SStep “по частинах” (множини “однотипних” перетворень). Паралельне програмування. Розподілені системи і мережі 125 1. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1–1, s2+1, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, sem (T, P) := (T +1, P +1) (d)) ) | s1>0 & iN16  siN } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), то Inv(S’) = (s3+s4+s5+s61) & ((s2+1)+s3+s4+s5+s6+s7+s8+s9+s10=P(d’)) & ( (A(d’)=0)  ( (A(d’)=1) & (s5=0) & (s6=0) ) ), де d’ = sem (T, P) := (T +1, P +1) (d) = d  [ T  (T(d) + 1), P  (P(d) + 1) ]. Таким чином, P(d’) = P(d) + 1, а A(d’) = A(d). Звідси, Inv(S’) = (s3+s4+s5+s61) & ((s2+1)+s3+s4+s5+s6+s7+s8+s9+s10=P(d)+1) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 2. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2–1, s3+1, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s2>0 & iN16  siN & sem P = 1 (d)=True } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem P = 1 (d) = (P(d) = 1) = True, тобто P(d) = 1, то з (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)), P(d) = 1 та s2>0 випливає, що s2=1 та s3=s4=s5=s6=s7=s8=s9=s10=0, тоді, враховуючи ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, Inv(S’) = ((s3+1)+s4+s5+s61) & ((s2–1)+(s3+1)+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True. 3. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2–1, s3, s4, s5, s6, s7, s8, s9, s10+1, s11, s12, s13, s14, s15, s16, d) ) | s2>0 & iN16  siN & sem P = 1 (d)=False }  якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem P = 1 (d) = (P(d) = 1) = False, то Inv(S’) = (s3+s4+s5+s61) & ((s2–1)+s3+s4+s5+s6+s7+s8+s9+(s10+1)=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 4. Розглянемо (S, S’)SStep : Паралельне програмування. Розподілені системи і мережі 126 { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3–1, s4+1, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s3>0 & iN16  siN & sem B = 0 (d)=True } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem B = 0 (d) = (B(d) = 0) = True, то Inv(S’) = ((s3–1)+(s4+1)+s5+s61) & (s2+(s3–1)+(s4+1)+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 5. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3–1, s4, s5, s6, s7, s8, s9+1, s10, s11, s12, s13, s14, s15, s16, d) ) | s3>0 & iN16  siN & sem B = 0 (d)=False } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem B = 0 (d) = (B(d) = 0) = False, то легко побачити, що Inv(S’) = ((s3–1)+s4+s5+s61) & (s2+(s3–1)+s4+s5+s6+s7+s8+(s9+1)+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, адже з Inv(S) логічно випливає Inv(S’). 6. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4–1, s5+1, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s4>0 & iN16  siN & sem A = 0 (d)=True } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem A = 0 (d) = (A(d) = 0) = True, тобто A(d) = 0, то Inv(S’) = (s3+(s4–1)+(s5+1)+s61) & (s2+s3+(s4–1)+(s5+1)+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & ((s5+1)=0) & (s6=0) ) ) = True, адже перші два кон’юнкти – істинні з передумови (Inv(S) = True), а третій – оскільки A(d) = 0. 7. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4–1, s5, s6, s7, s8+1, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s4>0 & iN16  siN & sem A = 0 (d)=False } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem A = 0 (d) = (A(d) = 0) = False, то Паралельне програмування. Розподілені системи і мережі 127 Inv(S’) = (s3+(s4–1)+s5+s61) & (s2+s3+(s4–1)+s5+s6+s7+(s8+1)+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True (з Inv(S) логічно випливає Inv(S’)). 8. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5–1, s6+1, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s5>0 & iN16  siN & sem data_provided_correct() (d)=True } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem data_provided_correct() (d) = (choice (True, False)) = True, звідси, враховуючи s5>0, маємо s5=1 та s3=s4=s6=0 (випливає з істинності першого кон’юнкта Inv(S)), звідси ( (A(d)=1) & (s5=0) & (s6=0) ) = False, тому (A(d)=0) = True, щоб ( (A(d)=0)  ( (A(d)=1) & (s5=0) &(s6=0) ) ) = True, тоді, очевидно, Inv(S’) = (s3+s4+(s5–1)+(s6+1)1) & (s2+s3+s4+(s5–1)+(s6+1)+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & ((s5–1)=0) & ((s6+1)=0) ) ) = True. 9. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5–1, s6, s7+1, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s5>0 & iN16  siN & sem data_provided_correct() (d)=False } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem data_provided_correct() (d) = (choice (True, False)) = False, звідси, враховуючи s5>0, маємо s5=1 та s3=s4=s6=0 (випливає з істинності першого кон’юнкта Inv(S)), звідси ( (A(d)=1) & (s5=0) & (s6=0) ) = False, тому (A(d)=0) = True, щоб третій кон’юнкт ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, тоді Inv(S’) = (s3+s4+(s5–1)+s61) & (s2+s3+s4+(s5–1)+s6+(s7+1)+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & ((s5–1)=0) & (s6=0) ) ) = True (перший і другий кон’юнкти випливають з Inv(S), а третій є істинним за рахунок (A(d)=0) = True). 10. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6–1, s7, s8, s9, s10, s11+1, s12, s13, s14, s15, s16, sem (A, P) := (A +1, P –1) (d)) ) | s6>0 & iN16  siN } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також s6>0, то Inv(S’) = (s3+s4+s5+(s6–1)1) & (s2+s3+s4+s5+(s6–1)+s7+s8+s9+s10=P(d’)) & ( (A(d’)=0)  ( (A(d’)=1) & (s5=0) & ((s6–1)=0) ) ), де Паралельне програмування. Розподілені системи і мережі 128 d’ = sem (A, P) := (A +1, P –1) (d) = d  [ A  (A(d) + 1), P  (P(d) – 1) ]. Таким чином, P(d’) = P(d) – 1, а A(d’) = A(d) + 1. Тепер, з Inv(S) = True випливає, що s3+s4+s5+s61, s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d) та (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) = True. Оскільки s6>0, то True = ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) & (s6>0) = (A(d)=0) & (s6>0)  (A(d)=1) & (s5=0) & (s6=0) & (s6>0) = (A(d)=0) & (s6>0)  False = (A(d)=0) & True = (A(d)=0). Далі, за визначенням спрощеного стану, перші 16 компонент є невід’ємними цілими числами, а отже, з s3+s4+s5+s61 та s6>0 випливає, що s6=1 та s3=s4=s5=0. Звідси, Inv(S’) = (s3+s4+s5+(s6–1)1) & (s2+s3+s4+s5+(s6–1)+s7+s8+s9+s10=P(d)–1) & ( (A(d)+1=0)  ( (A(d)+1=1) & (s5=0) & ((s6–1)=0) ) ). Перші два кон’юнкти мають значення True (очевидно, випливає з Inv(S) = True). Далі, з A(d)=0, s5=0 та s6=1 випливає, що (A(d)+1=1) & (s5=0) & ((s6–1)=0) = True, тобто і третій кон’юнкт має значення True. Таким чином, Inv(S’) = True. 11. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7–1, s8, s9, s10, s11+1, s12, s13, s14, s15, s16, sem P := P –1 (d)) ) | s7>0 & iN16  siN } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), то Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+(s7–1)+s8+s9+s10=P(d’)) & ( (A(d’)=0)  ( (A(d’)=1) & (s5=0) & (s6=0) ) ), де d’ = sem P := P –1 (d) = d  [ P  (P(d) – 1) ]. Таким чином, P(d’) = P(d) – 1, а A(d’) = A(d). Звідси, Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+(s7–1)+s8+s9+s10=P(d)–1) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 12. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8–1, s9, s10, s11+1, s12, s13, s14, s15, s16, sem P := P –1 (d)) ) | s8>0 & iN16  siN } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), то Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+(s8–1)+s9+s10=P(d’)) & ( (A(d’)=0)  ( (A(d’)=1) & (s5=0) & (s6=0) ) ), де d’ = sem P := P –1 (d) = d  [ P  (P(d) – 1) ]. Таким чином, P(d’) = P(d) – 1, а A(d’) = A(d). Звідси, Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+(s8–1)+s9+s10=P(d)–1) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 13. Розглянемо (S, S’)SStep : Паралельне програмування. Розподілені системи і мережі 129 { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9–1, s10, s11+1, s12, s13, s14, s15, s16, sem P := P –1 (d)) ) | s9>0 & iN16  siN } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), то Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+(s9–1)+s10=P(d’)) & ( (A(d’)=0)  ( (A(d’)=1) & (s5=0) & (s6=0) ) ), де d’ = sem P := P –1 (d) = d  [ P  (P(d) – 1) ]. Таким чином, P(d’) = P(d) – 1, а A(d’) = A(d). Звідси, Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+(s9–1)+s10=P(d)–1) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 14. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10–1, s11+1, s12, s13, s14, s15, s16, sem P := P –1 (d)) ) | s10>0 & iN16  siN } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), то Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+(s10–1)=P(d’)) & ( (A(d’)=0)  ( (A(d’)=1) & (s5=0) & (s6=0) ) ), де d’ = sem P := P –1 (d) = d  [ P  (P(d) – 1) ]. Таким чином, P(d’) = P(d) – 1, а A(d’) = A(d). Звідси, Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+(s10–1)=P(d)–1) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 15. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11–1, s12+1, s13, s14, s15, s16, d) ) | s11>0 & iN16  siN & sem T > 2 (d)=True } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem T > 2 (d) = (T(d) > 2) = True, то Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 16. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11–1, s12, s13+1, s14, s15, s16, d) ) | s11>0 & iN16  siN & sem T > 2 (d)=False } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, Паралельне програмування. Розподілені системи і мережі 130 де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem T > 2 (d) = (T(d) > 2) = False, то Inv(S’) = (s3+s4+s5+s61) & (s2+ s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 17. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12–1, s13, s14+1, s15, s16, sem B := 1 (d)) ) | s12>0 & iN16  siN } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), то Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d’)) & ( (A(d’)=0)  ( (A(d’)=1) & (s5=0) & (s6=0) ) ), де d’ = sem B := 1 (d) = d  [ B  1 ]. Таким чином, P(d’) = P(d), а A(d’) = A(d). Звідси, Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 18. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13–1, s14+1, s15, s16, sem Id (d)) ) | s13>0 & iN16  siN } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), то Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d’)) & ( (A(d’)=0)  ( (A(d’)=1) & (s5=0) & (s6=0) ) ), де d’ = sem Id (d) = d. Таким чином, P(d’) = P(d), а A(d’) = A(d). Звідси, Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 19. Розглянемо (S, S’)SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15–1, s16+1, sem B := 0 (d)) ) | s15>0 & iN16  siN } якщо Inv(S) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), то Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d’)) & ( (A(d’)=0)  ( (A(d’)=1) & (s5=0) & (s6=0) ) ), де d’ = sem B := 0 (d) = d  [ B  0 ]. Паралельне програмування. Розподілені системи і мережі 131 Таким чином, P(d’) = P(d), а A(d’) = A(d). Звідси, Inv(S’) = (s3+s4+s5+s61) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P(d)) & ( (A(d)=0)  ( (A(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. Доведення завершене. Маємо: - SSStartStates  ( PreCond(S)  Inv(S) ), - SSStates  ( Inv(S)  PostCond(S) ), - (S, S’)SStep  ( Inv(S)  Inv(S’) ). Тобто, InvCond(Inv, PreCond, PostCond) = True. Звідси {A1} Program {A1}. Очевидно, що SSStartStates  PreCond(S), адже на початку роботи Program записів в таблиці Auth немає і [ A  0 ]. Тоді автоматично отримаємо SSStopStates  PostCond(S) як наслідок щойно доведеного InvCond(Inv, PreCond, PostCond) = True. Але SSStates  ( Inv(S)  PostCond(S) ), звідси необхідна умова (PostCond(S)) виконується на кожному досяжному кроці виконання програми Program. Тобто, фактично, було доведено більш сильне твердження – а саме, що програма є коректною і не порушує за- дану умову (A1) не лише на початку і в кінці, а і на протязі всього часу виконання, тобто на кожному кроці. Тотальна коректність Оскільки програма не має циклів, ані блокувань, ані інших затримуючих або непередбачуваних факторів, які можуть «зациклити», або зупинити, або якимось чином затримати виконання – вона обов’язково завершить роботу за скінчену кількість кроків. Очевидне обмеження на кількість кроків – n * 9 + m, де 9 – діаметр графу переходів між мітками програми Auth_Prog. Висновки Застосовано спрощений метод [7] доведення властивостей interleaving concurrency програм у IPCL [1–3] для доведення властивості коректної роботи банківської системи виплати міжнародних грошових переказів. Це доведення є черговим підтвердженням [8–10] та демонстрацією зручності та адекватності застосування методу для доведення властивостей програмних систем, що виконуються у режимі паралелізму з переключенням та взаємодіють через спільну пам’ять – наприклад, серверних компонент клієнт-серверних комплексів, програм у архітектурі SMP та паралельних середовищ на кшталт суперкомп’ютерів. 1. Панченко Т.В. Метод доведення властивостей програм в композиційно-номінативних мовах IPCL // Проблеми програмування. – 2008. – №1. – С. 3–16. 2. Панченко Т.В. Методологія доведення властивостей програм в композиційних мовах IPCL // Доповіді Міжнародної конференції “Тео- ретичні та прикладні аспекти побудови програмних систем” (TAAPSD’2004). – К., 2004. – С. 62–67. 3. Панченко Т.В. Композиційні методи специфікації та верифікації програмних систем. – Автореферат дис. … канд. фіз.-мат. наук. – К., 2006. – 17 с. 4. Беренсон Х., Бернштейн Ф., Грэй Д. и др. Критика уровней изолированности в стандарте ANSI SQL // СУБД. – 1996. – № 2. – С. 45–60. 5. Редько В.Н., Брона Ю.Й., Буй Д.Б., Поляков С.А. Реляційні бази даних: табличні алгебри та SQL-подібні мови. – К.: Видавничий дім “Академперіодика”, 2001. – 198 с. 6. Басараб И.А., Никитченко Н.С., Редько В.Н. Композиционные базы данных. – К.: Либідь, 1992. – 191 с. 7. Панченко Т.В. Модель спрощеного стану для методу доведення властивостей в мовах IPCL та її застосування і переваги // Доповіді міжнародної наукової конференції TAAPSD`2007. – Berdyansk, 2007. – С. 319–322. 8. Polishchuk N.V., Kartavov M.O. and Panchenko T.V. Safety Property Proof using Correctness Proof Methodology in IPCL // Proceedings of the 5th International Scientific Conference “Theoretical and Applied Aspects of Cybernetics”. – Kyiv: Bukrek, 2015. – P. 37–44. Паралельне програмування. Розподілені системи і мережі 132 9. Картавов М.О., Панченко Т.В., Поліщук Н.В. Доведення тотальної коректності системи Infosoft e-Detailing у IPCL // Вісник Київського національного університету імені Тараса Шевченка. Серія: фіз.-мат. науки. – 2015. – Вип. 3. – С. 80–83. 10. Kartavov M. Properties Proof Method in IPCL Application To Real-World System Correctness Proof / M. Kartavov, T. Panchenko, N. Polishchuk // International Journal "Information Models and Analyses". – Sofia, Bulgaria: ITHEA. – 2015. – Vol. 4, N 2. – P. 142–155. References 1. PANCHENKO, T. (2008) The Method for Program Properties Proof in Compositional Nominative Languages IPCL [in Ukrainian]. Problems of Programming. 1. pp. 3–16. 2. PANCHENKO, T. (2004) The Methodology for Program Properties Proof in Compositional Languages IPCL [in Ukrainian]. In Proceedings of the International Conference "Theoretical and Applied Aspects of Program Systems Development" (TAAPSD'2004). Kyiv. pp. 62–67. 3. PANCHENKO, T. (2006) Compositional Methods for Software Systems Specification and Verification (PhD Thesis Synopsis) [in Ukrainian]. Kyiv. 17 p. 4. BERENSON, Kh., BERNSTEIN, F. And GREY, D. (1996) Critique of Isolation Levels in ANSI SQL Standard [in Russian]. DBMS, no. 2, pp. 45–60. 5. REDKO, V., BRONA, Yu., BUY, D. and POLYAKOV, S. (2001) Relational Databases: Table Algebras and SQL-like Languages [in Ukrainian]. Kyiv, “Akademperiodika”, 198 p. 6. BASARAB, I., NIKITCHENKO, M. and REDKO, V. (1992) Compositional Databases [in Russian]. Kyiv, “Lybid”, 191 p. 7. PANCHENKO, T. (2007) The Simplified State Model for Properties Proof Method in IPCL Languages and its use and advantages [in Ukrainian]. In Proceedings of the International Conference "Theoretical and Applied Aspects of Program Systems Development" (TAAPSD'2007). Berdyansk. pp. 319–322. 8. POLISHCHUK, N.V., KARTAVOV, M.O. and PANCHENKO, T.V. (2015) Safety Property Proof using Correctness Proof Methodology in IPCL. In Proceedings of the 5th International Scientific Conference “Theoretical and Applied Aspects of Cybernetics”, Kyiv, Bukrek, pp.37-44. 9. KARTAVOV, M.O., PANCHENKO, T.V. and POLISHCHUK, N.V. (2015) Infosoft e-Detailing System Total Correctness Proof in IPCL [in Ukrainian], Bulletin of Taras Shevchenko National University of Kyiv. Series: Physical and Mathematical Sciences, no. 3, pp. 80–83. 10. KARTAVOV, M., PANCHENKO, T. and POLISHCHUK, N. (2015) Properties Proof Method in IPCL Application To Real-World System Correctness Proof. International Journal "Information Models and Analyses", Sofia, Bulgaria, ITHEA, Vol. 4, no. 2, pp. 142–155. Про авторів: Остаповська Юлія Аркадіївна, студентка 4 курсу кафедри Теорії та технології програмування факультету кібернетики. Кількість наукових публікацій в українських виданнях – 1. http://orcid.org/0000-0002-8865-2139, Панченко Тарас Володимирович, кандидат фізико-математичних наук, доцент, доцент кафедри Теорії та технології програмування факультету кібернетики. Кількість наукових публікацій в українських виданнях – 27. Кількість наукових публікацій в іноземних виданнях – 2. http://orcid.org/0000-0003-0412-1945, Поліщук Наталія Володимирівна, студентка 4 курсу кафедри Теорії та технології програмування факультету кібернетики. Кількість наукових публікацій в українських виданнях – 3. Кількість наукових публікацій в іноземних виданнях – 1. http://orcid.org/0000-0001-6936-0053, Картавов Микита Олексійович, студент 4 курсу кафедри Теорії та технології програмування факультету кібернетики. Кількість наукових публікацій в українських виданнях – 3. Кількість наукових публікацій в іноземних виданнях – 1. http://orcid.org/0000-0002-2020-3468. Місце роботи авторів: Київський національний університет імені Тараса Шевченка, 03680, Київ, проспект Академіка Глушкова, 4Д. Тел.: 259 0519. E-mail: tp@infosoft.ua

Схожі ресурси