Please use this identifier to cite or link to this item:
https://open.uns.ac.rs/handle/123456789/3016
Title: | An approach to formal verification of python software transactional memory | Authors: | Kordić, Branislav Popović, Miroslav Gilezan, Silvia Bašičević, Ilija |
Issue Date: | 31-Aug-2017 | Journal: | ACM International Conference Proceeding Series | Abstract: | © 2017 ACM. Although Python is one of the most widely used programming languages, and it is a foundation for a variety of parallel and distributed computing frameworks, it still lacks an applicable and reliable software transactional memory. In this paper, we present an approach to formal verification of a Python Software Transactional Memory (PSTM) solution using UPPAAL tool. The aims are (i) to apply a formal verification process to a real STM implementation in order to derive a faithful STM model based on a PSTM design and (ii) to use developed PSTM model for automated machine-checked formal verification of core system properties such as safety and liveness using a model checker tool. Firstly, an architecture of PSTM solution is introduced. Secondly, formalization and a PSTM system model are analyzed. Finally, core PSTM system's properties are verified, namely safety, liveness, and reachability. Utilizing a UPPAAL's model checker tool it is successfully verified that the PSTM system model satisfies each of the three formerly mentioned properties. | URI: | https://open.uns.ac.rs/handle/123456789/3016 | ISBN: | 9781450348430 | DOI: | 10.1145/3123779.3123788 |
Appears in Collections: | FTN Publikacije/Publications |
Show full item record
SCOPUSTM
Citations
8
checked on May 20, 2023
Page view(s)
50
Last Week
2
2
Last month
2
2
checked on Mar 15, 2024
Google ScholarTM
Check
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.