Молимо вас користите овај идентификатор за цитирање или овај линк до ове ставке:
https://open.uns.ac.rs/handle/123456789/12783
Назив: | Formal verification of python software transactional memory based on timed automata | Аутори: | Kordić, Branislav Popović, Miroslav Gilezan, Silvia |
Датум издавања: | 1-јан-2019 | Часопис: | Acta Polytechnica Hungarica | Сажетак: | © 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 |
Налази се у колекцијама: | FTN Publikacije/Publications |
Приказати целокупан запис ставки
Преглед/и станица
106
Протекла недеља
30
30
Протекли месец
8
8
проверено 03.05.2024.
Google ScholarTM
Проверите
Алт метрика
Ставке на DSpace-у су заштићене ауторским правима, са свим правима задржаним, осим ако није другачије назначено.