Correctness Property Proof for the Banking System for Money Transfer Payments

Yu.A. Ostapovska, T.V. Panchenko, N.V. Polishchuk, M.O. Kartavov

Abstract


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


Keywords


software correctness; safety property proof; concurrent program; interleaving; invariant; IPCL; composition-nominative languages; formal verification

References


PANCHENKO, T. (2008) The Method for Program Properties Proof in Compositional Nominative Languages IPCL [in Ukrainian]. Problems of Programming. 1. pp. 3–16.

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.

PANCHENKO, T. (2006) Compositional Methods for Software Systems Specification and Verification (PhD Thesis Synopsis) [in Ukrainian]. Kyiv. 17 p.

BERENSON, Kh., BERNSTEIN, F. And GREY, D. (1996) Critique of Isolation Levels in ANSI SQL Standard [in Russian]. DBMS, no. 2, pp. 45–60. https://doi.org/10.1145/568271.223785

REDKO, V., BRONA, Yu., BUY, D. and POLYAKOV, S. (2001) Relational Databases: Table Algebras and SQL-like Languages [in Ukrainian]. Kyiv, “Akademperiodika”, 198 p.

BASARAB, I., NIKITCHENKO, M. and REDKO, V. (1992) Compositional Databases [in Russian]. Kyiv, “Lybid”, 191 p.

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.

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.

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.

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.




DOI: https://doi.org/10.15407/pp2016.02-03.119

Refbacks

  • There are currently no refbacks.