Debugger interface for Java PathFinder model checker

• Název práce v češtině: Debugger interface pro Java PathFinder model checker
• Název v anglickém jazyce: Debugger interface for Java PathFinder model checker
• Klíčová slova: debugování, Java PathFinder, Java Debug Wire Protocol agent, Java Platform Debugger Architecture
• Klíčová slova anglicky: debugging, Java PathFinder, Java Debug Wire Protocol Agent, Java Platform Debugger Architecture
• Akademický rok vypsání: 2012/2013
• Typ práce: diplomová práce
• Jazyk práce: angličtina
• Ústav: Katedra distribuovaných a spolehlivých systémů (32-KDSS)
• Vedoucí / školitel: Mgr. Pavel Jančík, Ph.D.
• Řešitel: skrytý - zadáno a potvrzeno stud. odd.
• Datum přihlášení: 15.03.2013
• Datum zadání: 15.03.2013
• Datum potvrzení stud. oddělením: 22.03.2013
• Datum a čas obhajoby: 27.01.2014 09:00
• Datum odevzdání elektronické podoby: 06.12.2013
• Datum odevzdání tištěné podoby: 06.12.2013
• Datum proběhlé obhajoby: 27.01.2014
• Oponenti: RNDr. Jakub Yaghob, Ph.D.

Zásady pro vypracování

Java PathFinder is a state-of-the-art code model checker developed by NASA. It is a JVM specialized for the detection of low-lever errors and races (scheduling dependent bugs).
The goal of this thesis is to implement the Java Platform Debugger Architecture for JPF so that standard IDEs can be used to debug programs being verified, which is demanded by JPF users. Using standard debugging facilities of the IDE will help users to understand the errors found by JPF, ease the development of new extensions, models of environments, and also ease detection of the roots of state-space explosion.
In the thesis the author should also document and solve issues arisen by specific properties of the JPF not expected by JPDA. The implementation should be integrated into common Java IDE (preferably Eclipse).

Seznam odborné literatury

Java PathFinder - http://babelfish.arc.nasa.gov/trac/jpf
Java Platform Debugger Architecture - http://java.sun.com/javase/technologies/core/toolsapis/jpda/

Předběžná náplň práce v anglickém jazyce

Java PathFinder is a state-of-the-art code model checker developed by NASA. It is a JVM specialized for detection of low-lever errors and races (scheduling dependent bugs).
The goal of this thesis is to create a debugger for the JPF virtual machine, which is demanded by JPF users. The debugger will help users to understand the errors found by JPF, will ease the development of new extensions, models of environments, as well as the detection of the roots of state-space explosion.
The main part of the work consists of the implementation of the Java Platform Debugger Architecture, so that standard IDEs can be used to debug programs executed by JPF.
The implementation should be integrated into Eclipse IDE (possibly using eclipse-jpf project) to start debugging easily.