Thesis Details

Bounded model checking v nástroji Java PathFinder

Master's Thesis Student: Dudka Vendula Academic Year: 2007/2008 Supervisor: Křena Bohuslav, Ing., Ph.D.
English title
Bounded Model Checking Using Java PathFinder
Language
Czech
Abstract

This thesis deals with the application of bounded model checkingmethod for self-healing assurance of concurrency related problems. The self-healing is currently interested in the Java programming language. Therefore, it concetrate mainly on the model checker Java PathFinder which is built for handling Java programs. The verification method is implemented like the Record&Replay trace strategy for navigation through a state space and performance bounded model checking from reached state through the use of Record&Replay trace strategy. Java PathFinder was extended by new moduls and interfaces in order to perform the bounded model checking for self-healing assurance. Bounded model checking is applied at the neighbourhood of self-healing.

Keywords

Model Checking, Java PathFinder, Bounded model checking, verification, Record&Replay trace, self-healing, concurrency, healing assurance

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology, Field of Study Computer Graphics and Multimedia
Files
Status
defended, grade B
Date
17 June 2008
Reviewer
Češka Milan, prof. RNDr., CSc.
Committee
Meduna Alexander, prof. RNDr., CSc. (DIFS FIT BUT), předseda
Černocký Jan, prof. Dr. Ing. (DCGM FIT BUT), člen
Fučík Otto, doc. Dr. Ing. (DCSY FIT BUT), člen
Kršek Přemysl, doc. Ing., Ph.D. (DCGM FIT BUT), člen
Sochor Jiří, prof. Ing., CSc. (FI MUNI), člen
Zemčík Pavel, prof. Dr. Ing. (DCGM FIT BUT), člen
Citation
DUDKA, Vendula. Bounded model checking v nástroji Java PathFinder. Brno, 2008. Master's Thesis. Brno University of Technology, Faculty of Information Technology. 2008-06-17. Supervised by Křena Bohuslav. Available from: https://www.fit.vut.cz/study/thesis/6443/
BibTeX 
@mastersthesis{FITMT6443,
    author = "Vendula Dudka",
    type = "Master's thesis",
    title = "Bounded model checking v n\'{a}stroji Java PathFinder",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2008,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/6443/"
}

Theses

Back to top