Authors: Kordić, Branislav
Popović, Miroslav
Ghilezan, Silvia 
Title: Formal verification of python software transactional memory based on timed automata
Journal: Acta Polytechnica Hungarica
Volume: 16
Issue: 7
First page: 197
Last page: 216
Issue Date: 1-Jan-2019
Rank: M22
ISSN: 1785-8860
DOI: 10.12700/APH.16.7.2019.7.12
Nowadays Software Transactional Memories (STMs) are used in safety-critical software, such as computational-chemistry simulation programs. To the best of our knowledge, the existing STMs were not developed using rigorous model-driven development process, on the contrary, the majority of proposed STMs are directly implemented in a target programming language and formally verified STMs are proven against more general models. This may result in some key aspects of implementation being omitted or interpreted incorrectly. In this paper, we demonstrate an approach to the formal verification of one particular STM, for the Python language, named Python Software Transactional Memory (PSTM), which is based on a STM design and implementation details. Based on these details, faithful models of a PSTM based system, are developed and verified. The PSTM system components are modeled as timed automata utilizing UPPAAL tool. Finally, it is verified that PSTM satisfies deadlock-freeness, safety, liveness, and reachability properties.
Keywords: Correctness | Formal verification | Model checking | Timed automata | Transactional memory
Publisher: Budapest Tech Polytechnical Institution
Project: 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 
Development of embedded systems with connected services and digital technology 
Representations of logical structures and formal languages and their application in computing 

Show full item record


checked on May 21, 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.