Témata prací (Výběr práce)Témata prací (Výběr práce)(verze: 368)
Detail práce
   Přihlásit přes CAS
Presenting results of software model checker via debugging interface
Název práce v češtině: Presenting results of software model checker via debugging interface
Název v anglickém jazyce: Presenting results of software model checker via debugging interface
Klíčová slova: Java, verifikace, kontrola modelu, JPF, ladící rozhraní
Klíčová slova anglicky: Java, verification, model checker, JPF, debugging interface
Akademický rok vypsání: 2011/2012
Typ práce: diplomová práce
Jazyk práce: angličtina
Ústav: Katedra softwarového inženýrství (32-KSI)
Vedoucí / školitel: RNDr. Ondřej Šerý, Ph.D.
Řešitel: skrytý - zadáno a potvrzeno stud. odd.
Datum přihlášení: 31.07.2012
Datum zadání: 31.07.2012
Datum potvrzení stud. oddělením: 31.07.2012
Datum a čas obhajoby: 03.09.2012 09:00
Datum odevzdání elektronické podoby:02.08.2012
Datum odevzdání tištěné podoby:03.08.2012
Datum proběhlé obhajoby: 03.09.2012
Oponenti: Mgr. Pavel Jančík, Ph.D.
 
 
 
Zásady pro vypracování
The software model checker allows automatic detection of flaws in software systems. In particular, the model checker provides a proof that the program is correct in some sense. If the program is not correct, then the model checker provides a counter example, which is basically the history of program states leading to the errorneous state.

Currently, the model checkers are not widely used in mainstream development process. Beside other reasons, like the size of feasible programs, these tools are not very user friendly. Being the command-line tools, the counter examples are just printed out and their interpretation is up to the user.

On the other hand, the modern IDEs are excellent in presentation of a state of a paused program. The user is allowed to inspect the call stack of each thread together with the values of variables.

In particular, when speaking about Java Platform, the IDE communicates with the paused JVM through standard debugging API. The C++ often generates dumps, which may be later inspected by IDE.

The state of the program is a significant part of the counter example presented by the model checker.

The goal of this thesis is to implement standard debugging API into a mature model checker to allow inspection of the error state using mainstream IDE. The optional goal is to extend the API to provide further information from the counter example, like history of states resulting in the error.

The intended platform is Java Platform Debugger Architecture (JPDA) and Java PathFinder. However, the author may suggest alternatives.
Seznam odborné literatury
E. Clarke, O.Grumberg, D. Peled: Model Checking, ISBN-13: 9780262032704

"The Java(TM) Language Specification (3rd Edition)" James Gosling, Bill Joy, Guy Steele, Gilad Bracha
"Model Checking Programs". W. Visser, K. Havelund, G. Brat, S. Park and F. Lerda. Automated Software Engineering Journal.Volume 10, Number 2, April 2003.
"Pro NetBeans IDE 6 Rich Client Platform Edition" Adam Myatt, Brian Leonard and Geertjan Wielenga. ISBN: 1590598954
Java Platform Debugging Architecture : http://java.sun.com/javase/6/docs/technotes/guides/jpda/index.html
 
Univerzita Karlova | Informační systém UK