Open AccessCorrectness Property Proof for the Banking System for Money Transfer Payments
Author(s) -
Yu.A. Ostapovska,
T. V. Panchenko,
N.V. Polishchuk,
M.O. Kartavov
Publication year - 2016
Publication title -
problemy programmirovaniâ
Language(s) - English
Resource type - Journals
ISSN - 1727-4907
DOI - 10.15407/pp2016.02-03.119
Subject(s) - correctness , payment , interleaving , computer science , property (philosophy) , task (project management) , invariant (physics) , algorithm , mathematics , operating system , economics , world wide web , mathematical physics , management , philosophy , epistemology
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.