Формална верификација софтверске трансакционе меморије засноване на временским аутоматима

Abstract

Основни циљ истраживања дисертације је примена формализма временских аутомата за моделовање и формалну верификацију софтверске трансакционе меморије (СТМ) који се заснива на детаљима архитектуре и имплементације користећи изворни код решења. Исправност СТМ модела се утврђује машинским (аутоматским) путем употребом алата за проверу исправности модела. Моделовање СТМ, а потом и формална верификација њене исправности, је урађено употребом алата УППААЛ. Верификацијом развијених модела желе се проверити својства исправности, као што су својства сигурности, животности и достижности. Поступак примене је представљен на примеру конкретне имплементације СТМ за програмски језик Пајтон (ПСТМ). Резултати су утврдили да ПСТМ задовољава сва од претходно наведених својстава. Такође, по најбољем сазнању аутора, ПСТМ представља прву формално верификовану СТМ за програмски језик Пајтон.

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 formal verification of a software transactional memory (STM) using timed automata formalism which is based on a STM design and implementation details using source code. Correctness of STM model is formally verified in automated and machine-checked manner using a model checker tool. STM models are modeled and verified using UPPAAL tool. The formal verification of the STM models aims to check the correctness of system properties, such as safety, liveness and reachability. The formal verification approach is validated using particular STM for Python, named Python Software Transactional Memory (PSTM). Verification results show that PSTM satisfies all of the above mentioned properties. Also, to the best of author’s knowledge, PSTM is the first formally verified STM for the Python programming language.