Correctness Property Proof for the Banking System for Money Transfer Payments

• Veröffentlicht in: PROBLEMS IN PROGRAMMING
• Datum: 2018
• Heft: 2-3
• Сторінки: 119-132
• ISSN: 1727-4907
• Автори та афіліації: Yu.A. Ostapovska — Kiev Taras Shevchenko National University; T.V. Panchenko — Kiev Taras Shevchenko National University; N.V. Polishchuk — Kiev Taras Shevchenko National University; M.O. Kartavov — Kiev Taras Shevchkenko National University
• Ключові слова: доведення часткової коректності, коректність програмного забезпечення, паралельна програма, формальна верифікація, ipcl, розподілені системи та паралельне програмування, програмний комплекс “інтеграл”, синхронізація паралельних програм, верифікація, частковий предикат
• Hauptverfasser: Ostapovska, Yu.A., Panchenko, T.V., Polishchuk, N.V., Kartavov, M.O.
• Format: Artikel
• Sprache: Ukrainisch
• Veröffentlicht: PROBLEMS IN PROGRAMMING 2018
• Schlagworte: software correctness; safety property proof; concurrent program; interleaving; invariant; IPCL; composition-nominative languages; formal verification; UDC 004.415.52
• Online Zugang: https://pp.isofts.kiev.ua/index.php/ojs1/article/view/187
• Назва журналу: Problems in programming

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