|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||URL:||http://acta.uni-obuda.hu/Kordic_Popovic_Ghilezan_94.pdf||Abstract:||
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 Mar 26, 2023
checked on Mar 27, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.