Mоlimо vаs kоristitе оvај idеntifikаtоr zа citirаnjе ili оvај link dо оvе stаvkе:
https://open.uns.ac.rs/handle/123456789/12783
Nаziv: | Formal verification of python software transactional memory based on timed automata | Аutоri: | Kordić, Branislav Popović, Miroslav Gilezan, Silvia |
Dаtum izdаvаnjа: | 1-јан-2019 | Čаsоpis: | Acta Polytechnica Hungarica | Sažetak: | © 2019, Budapest Tech Polytechnical Institution. All rights reserved. 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. | URI: | https://open.uns.ac.rs/handle/123456789/12783 | ISSN: | 17858860 | DOI: | 10.12700/APH.16.7.2019.7.12 |
Nаlаzi sе u kоlеkciјаmа: | FTN Publikacije/Publications |
Prikаzаti cеlоkupаn zаpis stаvki
Stаvkе nа DSpace-u su zаštićеnе аutоrskim prаvimа, sа svim prаvimа zаdržаnim, оsim аkо nije drugačije naznačeno.