Authors: Kordić, Branislav
Popović, Miroslav
Ghilezan, Silvia 
Bašičević, Ilija
Title: An approach to formal verification of python software transactional memory
Journal: ACM International Conference Proceeding Series
Volume: Part F130524
Conference: 5th European Conference on the Engineering of Computer-Based Systems, ECBS 2017; Larnaca; Cyprus; 31 August 2017 through 1 September 2017
Issue Date: 31-Aug-2017
ISBN: 978-1-450-34843-0
DOI: 10.1145/3123779.3123788
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.
Keywords: Formal verification | Python | Software transactional memory | UPPAAL
Publisher: Association for Computing Machinery
Project: Software and tools for multi-core systems 
Representations of logical structures and formal languages and their application in computing 
Development of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and education 
Secretary of Science and Technology Development of the Province of Vojvodina, Grant 114-451-1074/2014-03

Show full item record


checked on May 23, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.