Using Java PathFinder for Construction of Abstractions of Java Programs
| Název práce v češtině: | Using Java PathFinder for Construction of Abstractions of Java Programs |
|---|---|
| Název v anglickém jazyce: | Using Java PathFinder for Construction of Abstractions of Java Programs |
| Akademický rok vypsání: | 2006/2007 |
| Typ práce: | diplomová práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra softwarového inženýrství (32-KSI) |
| Vedoucí / školitel: | doc. RNDr. Pavel Parízek, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 12.12.2006 |
| Datum zadání: | 12.12.2006 |
| Datum a čas obhajoby: | 25.05.2009 00:00 |
| Datum odevzdání elektronické podoby: | 25.05.2009 |
| Datum proběhlé obhajoby: | 25.05.2009 |
| Oponenti: | RNDr. Tomáš Poch, Ph.D. |
| Zásady pro vypracování |
| Java PathFinder is a multi-purpose verification tool for Java bytecode programs. It is mainly used as a software model checker, i.e. for checking whether a given Java bytecode program satisfies certain properties (absence of deadlocks, etc). Unlike most of model checkers that accept models of software systems as input, Java PathFinder works directly with the bytecode. However, main drawback of software model checking is that the state space of more complex software systems may be large enough to make checking not feasible. Common solution to this problem (of state explosion) is to create an abstraction of the target system, and then verify only the abstraction.
The goal of this thesis is to design and implement an extension of Java PathFinder that can be used to construct an abstraction (a model) of a software component implemented in Java. More specifically, the candidate should (1) select (or design) a simple abstraction of the Java language (e.g. LTS or behavior protocols), (2) design appropriate data structures for storing and processing of the model of a Java program, (3) implement an extension for Java PathFinder, and (4) try to find a way for making the process of construction of the model more efficient (e.g. via some heuristics), and discuss influence of the optimizations on the precision and completeness of the model. |
| Seznam odborné literatury |
| 1. Java PathFinder, http://javapathfinder.sourceforge.net
2. The SLAM Project, http://research.microsoft.com/slam 3. jMoped, http://www.fmi.uni-stuttgart.de/szs/tools/moped/jmoped/ 4. F. Plasil, S. Visnovsky: Behavior Protocols for Software Components. IEEE Transactions on Software Engineering, vol. 28, no. 11, Nov 2002 5. E. M. Clarke, D. Peled, O. Grumberg: Model Checking. MIT Press, 1999 |