Geodesic
Complete Formal Verification of the PSTM Transaction Scheduler
Computer Science and Information Systems, Tome 20 (2023) no. 1.

Voir la notice de l'article provenant de la source Computer Science and Information Systems website

State of the art formal verification is based on formal methods and its goal is proving given correctness properties. For example, a PSTM scheduler was modeled in CSP in order to prove deadlock-freeness and starvation-freeness. However, as this paper shows, using solely formal methods is not sufficient. Therefore, in this paper we propose a complete formal verification of trustworthy software, which jointly uses formal verification and formal model testing. As an example, we first test the previous CSP model of PSTM transaction scheduler by comparing the model checker PAT results with the manually derived expected results, for the given test workloads. Next, according to the results of this testing, we correct and extend the CSP model. Finally, using PAT results for the new CSP model, we analyze the performance of the PSTM online transaction scheduling algorithms from the perspective of the relative speedup.
Keywords: Formal Verification, Process Algebra, Transaction Scheduling, Python, Software Transactional Memory 
@article{CSIS_2023_20_1_a18,
     author = {Miroslav Popovic and Marko Popovic and Branislav Kordic and Huibiao Zhu},
     title = {Complete {Formal} {Verification} of the {PSTM} {Transaction} {Scheduler}},
     journal = {Computer Science and Information Systems},
     publisher = {mathdoc},
     volume = {20},
     number = {1},
     year = {2023},
     url = {http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a18/}
}
TY  - JOUR
AU  - Miroslav Popovic
AU  - Marko Popovic
AU  - Branislav Kordic
AU  - Huibiao Zhu
TI  - Complete Formal Verification of the PSTM Transaction Scheduler
JO  - Computer Science and Information Systems
PY  - 2023
VL  - 20
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a18/
ID  - CSIS_2023_20_1_a18
ER  - 
%0 Journal Article
%A Miroslav Popovic
%A Marko Popovic
%A Branislav Kordic
%A Huibiao Zhu
%T Complete Formal Verification of the PSTM Transaction Scheduler
%J Computer Science and Information Systems
%D 2023
%V 20
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a18/
%F CSIS_2023_20_1_a18
Miroslav Popovic; Marko Popovic; Branislav Kordic; Huibiao Zhu. Complete Formal Verification of the PSTM Transaction Scheduler. Computer Science and Information Systems, Tome 20 (2023) no. 1. http://geodesic.mathdoc.fr/item/CSIS_2023_20_1_a18/