Ověřování temporálních vlastností konečných běhů programů

Název anglicky

Checking of Temporal Properties of Finite Traces of Programs

Jazyk práce

český

Abstrakt

Temporální vlastnosti programů jsou používány ke specifikaci korektního průběhu jejich vykonávání. Jedním z nejčastějších způsobů formálního popisu těchto vlastností je lineární temporální logika - LTL, případně její varianty. Tato práce se zabývá návrhem a implementací nástroje pro automatizované ověřování temporálních vlastností běhů programů specifikovaných pomocí LTL minulého času (past-time LTL). Výsledný program na základě dané specifikace vygeneruje statickou knihovnu, která dokáže spolehlivě ověřit, zda jsou její formule v každém okamžiku běhu kontrolovaného programu splněny, a případné neočekávané nebo nesprávné chování hlásí společně s podrobnou zprávou o okolnostech tohoto chybového stavu, která má napomáhat k nalezení chyby v konkrétním místě kódu.

Klíčová slova

verifikace programů za běhu, temporální vlastnosti programů, lineární temporální logika

Ústav

Ústav inteligentních systémů FIT VUT v Brně

Studijní program

Informační technologie, obor Inteligentní systémy

Soubory

Stav

obhájeno, hodnocení A

Obhajoba

18. června 2019

Oponent

Češka Milan, doc. RNDr., Ph.D.

Průběh obhajoby

Studentka nejprve prezentovala výsledky, kterých dosáhla v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Studentka následně odpověděla na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studentky na položené otázky rozhodla práci hodnotit stupněm A.

Otázky u obhajoby

1) Je možné nástroj použít na monitorování libovolného C/C++ programu?
2) V práci uvádíte, že monitorování vede pouze k 2% zpomalení běhu programu. Předpokládáte, že podobné (tj. zanedbatelné) zpomalení bude nastávat u většiny programů a monitorů?

Komise

Zbořil František V., doc. Ing., CSc. (UITS FIT VUT), předseda
Beran Vítězslav, doc. Ing., Ph.D. (UPGM FIT VUT), člen
Grézl František, Ing., Ph.D. (UPGM FIT VUT), člen
Janoušek Jan, doc. Ing., Ph.D. (FIT ČVUT), člen
Peringer Petr, Dr. Ing. (UITS FIT VUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT), člen

Citace

SEČKAŘOVÁ, Petra. Ověřování temporálních vlastností konečných běhů programů. Brno, 2019. Diplomová práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2019-06-18. Vedoucí práce Smrčka Aleš. Dostupné z: https://www.fit.vut.cz/study/thesis/21762/

BibTeX

@mastersthesis{FITMT21762,
    author = "Petra Se\v{c}ka\v{r}ov\'{a}",
    type = "Diplomov\'{a} pr\'{a}ce",
    title = "Ov\v{e}\v{r}ov\'{a}n\'{i} tempor\'{a}ln\'{i}ch vlastnost\'{i} kone\v{c}n\'{y}ch b\v{e}h\r{u} program\r{u}",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2019,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/21762/"
}