Thesis Details

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

Master's Thesis Student: Sečkařová Petra Academic Year: 2018/2019 Supervisor: Smrčka Aleš, Ing., Ph.D.
English title
Checking of Temporal Properties of Finite Traces of Programs
Language
Czech
Abstract

Correct behavior of programs can be defined by their temporal properties. One of the options for formal specification of such properties is linear temporal logic - LTL. This master's thesis describes design and implementation of a tool for automatic checking of temporal properties of programs, that are specified using Past-Time LTL formulae. The trace of a given program is analyzed in run-time and any violation of given formulae is reported in details to help to find the code location with a root cause of the bug.

Keywords

run-time verification, temporal properties of programs, linear temporal logic

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology, Field of Study Intelligent Systems
Files
Status
defended, grade A
Date
18 June 2019
Reviewer
Češka Milan, doc. RNDr., Ph.D.
Committee
Zbořil František V., doc. Ing., CSc. (DITS FIT BUT), předseda
Beran Vítězslav, doc. Ing., Ph.D. (DCGM FIT BUT), člen
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Janoušek Jan, doc. Ing., Ph.D. (FIT CTU), člen
Peringer Petr, Dr. Ing. (DITS FIT BUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT), člen
Citation
SEČKAŘOVÁ, Petra. Ověřování temporálních vlastností konečných běhů programů. Brno, 2019. Master's Thesis. Brno University of Technology, Faculty of Information Technology. 2019-06-18. Supervised by Smrčka Aleš. Available from: https://www.fit.vut.cz/study/thesis/21762/
BibTeX 
@mastersthesis{FITMT21762,
    author = "Petra Se\v{c}ka\v{r}ov\'{a}",
    type = "Master's thesis",
    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 = "Brno University of Technology, Faculty of Information Technology",
    year = 2019,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/21762/"
}

Theses

Back to top