Název: Presenting results of software model checker via debugging interface
Překlad názvu: Presenting results of software model checker via debugging interface
Autoři: Kohan, Tomáš ; Šerý, Ondřej (vedoucí práce) ; Jančík, Pavel (oponent)
Typ dokumentu: Diplomové práce
Rok: 2012
Jazyk: eng
Abstrakt: [eng] [cze]
Title: Presenting results of software model checker via debugging interface Author: Tomáš Kohan Department: Department of Software Engineering Supervisor of the master thesis: RNDr. Ondřej Šerý, Ph.D., Department of Distributed and Dependable Systems Abstract: This thesis is devoted to design and implementation of the new debugging interface of the Java PathFinder application. As a suitable inte- face container was selected the Eclipse development environment. The created interface should visualize results of JPF and details of paused JVM state, es- pecially a list of variables and their values. Two subprojects were created, i.e. debug4jpf and JPFDeb.core. The first one is responsible for controlling and communication with the JPF instance. The latter one is an Eclipse plugin and provides user interface which is similar to the interface of standard Java debugger. These two components communicate with each other by using the ad-hoc communication protocol created for this purpose. Keywords: Java, verification, model checker, JPF, debugging interface Název práce: Prezentace výsledků kontroly softwarového modelu skrz ladící rozhraní Autor: Tomáš Kohan Katedra: Katedra softwarového inženýrství Vedoucí diplomové práce: RNDr. Ondřej Šerý, Ph.D., Katedra distribuovaných a spolehlivých systémů Abstrakt: Cílem této práce je navrhnout a implementovat nové ladící rozhraní programu Java PathFinder. Vhodným prostředím pro toto rozhraní byl zv- olen vývojový nástroj Eclipse. Vytvořené rozhraní graficky vizualizuje výstupy programu JPF a jednotlivé detaily stavu pozastaveného virtuálního stroje (JVM), zvláště pak seznam proměnných a jejich hodnot. Za tímto účelem jsou vytvořeny dva podprojekty, a to debug4jpg a JPFDeb.core. Projekt debug4jpf kontroluje a komunikuje s instancí JPF. JPFDeb.core pak ve formě zásuvného modulu pro Eclipse poskytuje takové uživatelské rozhraní, které je podobné standardnímu rozhraní ladícího programu pro Javu. Oba projekty mezi sebou komunikují přes ad hoc komunikační protokol, který byl navržen pro tento účel. Klíčová slova: Java, verifikace, kontrola modelu, JPF, ladící rozhraní
Klíčová slova: Java; JPF; kontrola modelu; ladící rozhraní; verifikace; debugging interface; Java; JPF; model checker; verification

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/41591

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-305891


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Diplomové práce