|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||Abstract:||
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 Mar 19, 2023
checked on Mar 20, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.