Formalna verifikacija softverske transakcione memorije zasnovane na vremenskim automatima
| Autor: | Kordić, Branislav |
|---|---|
| Přispěvatelé: | Popović, Miroslav, Teslić, Nikola, Tomašević, Milo, Gilezan, Silvia, Đukić, Miodrag |
| Jazyk: | srbština |
| Rok vydání: | 2020 |
| Předmět: |
Formalna verifikacija
softverske transakcione memorije provera modela ispravnost vremenski automati Pajton Formal verification software transactional memory model checking correctness timed automata Python Формална верификација софтверске трансакционе меморије провера модела исправност временски аутомати Пајтон |
| Zdroj: | CRIS UNS |
| Popis: | Основни циљ истраживања дисертације је примена формализма временских аутомата за моделовање и формалну верификацију софтверске трансакционе меморије (СТМ) који се заснива на детаљима архитектуре и имплементације користећи изворни код решења. Исправност СТМ модела се утврђује машинским (аутоматским) путем употребом алата за проверу исправности модела. Моделовање СТМ, а потом и формална верификација њене исправности, је урађено употребом алата УППААЛ. Верификацијом развијених модела желе се проверити својства исправности, као што су својства сигурности, животности и достижности. Поступак примене је представљен на примеру конкретне имплементације СТМ за програмски језик Пајтон (ПСТМ). Резултати су утврдили да ПСТМ задовољава сва од претходно наведених својстава. Такође, по најбољем сазнању аутора, ПСТМ представља прву формално верификовану СТМ за програмски језик Пајтон. Osnovni cilj istraživanja disertacije je primena formalizma vremenskih automata za modelovanje i formalnu verifikaciju softverske transakcione memorije (STM) koji se zasniva na detaljima arhitekture i implementacije koristeći izvorni kod rešenja. Ispravnost STM modela se utvrđuje mašinskim (automatskim) putem upotrebom alata za proveru ispravnosti modela. Modelovanje STM, a potom i formalna verifikacija njene ispravnosti, je urađeno upotrebom alata UPPAAL. Verifikacijom razvijenih modela žele se proveriti svojstva ispravnosti, kao što su svojstva sigurnosti, životnosti i dostižnosti. Postupak primene je predstavljen na primeru konkretne implementacije STM za programski jezik Pajton (PSTM). Rezultati su utvrdili da PSTM zadovoljava sva od prethodno navedenih svojstava. Takođe, po najboljem saznanju autora, PSTM predstavlja prvu formalno verifikovanu STM za programski jezik Pajton. The main goal of the PhD thesis research is an approach to formalverification of a software transactional memory (STM) using timed automataformalism which is based on a STM design and implementation details usingsource code. Correctness of STM model is formally verified in automated andmachine-checked manner using a model checker tool. STM models aremodeled and verified using UPPAAL tool. The formal verification of the STMmodels aims to check the correctness of system properties, such as safety,liveness and reachability. The formal verification approach is validated usingparticular STM for Python, named Python Software Transactional Memory(PSTM). Verification results show that PSTM satisfies all of the abovementioned properties. Also, to the best of author’s knowledge, PSTM is thefirst formally verified STM for the Python programming language. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|