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í: | 03.10.2011 |
| Datum zadání: | 03.10.2011 |
| Datum potvrzení stud. oddělením: | 16.03.2012 |
| Datum a čas obhajoby: | 28.05.2012 11:00 |
| Datum odevzdání elektronické podoby: | 11.04.2012 |
| Datum odevzdání tištěné podoby: | 13.04.2012 |
| Datum proběhlé obhajoby: | 28.05.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 |