Молимо вас користите овај идентификатор за цитирање или овај линк до ове ставке:
https://open.uns.ac.rs/handle/123456789/3016
Назив: | An approach to formal verification of python software transactional memory | Аутори: | Kordić, Branislav Popović, Miroslav Gilezan, Silvia Bašičević, Ilija |
Датум издавања: | 31-авг-2017 | Часопис: | ACM International Conference Proceeding Series | Сажетак: | © 2017 ACM. 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. | URI: | https://open.uns.ac.rs/handle/123456789/3016 | ISBN: | 9781450348430 | DOI: | 10.1145/3123779.3123788 |
Налази се у колекцијама: | FTN Publikacije/Publications |
Приказати целокупан запис ставки
SCOPUSTM
Навођења
8
проверено 10.05.2024.
Преглед/и станица
87
Протекла недеља
37
37
Протекли месец
2
2
проверено 10.05.2024.
Google ScholarTM
Проверите
Алт метрика
Ставке на DSpace-у су заштићене ауторским правима, са свим правима задржаним, осим ако није другачије назначено.