velikost textu

Formal Verfication of Components in Java

Upozornění: Informace získané z popisných dat či souborů uložených v Repozitáři závěrečných prací nemohou být použity k výdělečným účelům nebo vydávány za studijní, vědeckou nebo jinou tvůrčí činnost jiné osoby než autora.
Název:
Formal Verfication of Components in Java
Typ:
Disertační práce
Autor:
RNDr. Pavel Parízek, Ph.D.
Školitel:
prof. Ing. František Plášil, DrSc.
Oponenti:
Doc. RNDr. Ivana Černá, CSc.
Prof. Corina Pasareanu
Id práce:
43291
Fakulta:
Matematicko-fyzikální fakulta (MFF)
Pracoviště:
Katedra softwarového inženýrství (32-KSI)
Program studia:
Informatika (P1801)
Obor studia:
Softwarové systémy (4I2)
Přidělovaný titul:
Ph.D.
Datum obhajoby:
29. 9. 2008
Výsledek obhajoby:
Prospěl/a
Jazyk práce:
Angličtina
Abstract v angličtině:
Formal verication of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior specication and other properties like absence of concurrency errors. In this thesis, we focus on verication of primitive components implemented in Java against the properties of obeying a behavior specication dened in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core verication tool. We propose a set of techniques that address the key issues of formal verication of real-life components in Java via model checking: support for high-level property of obeying a behavior specication, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java bytecode and various heuristics. We have implemented all the techniques in the COMBAT toolset and evaluated them on two realistic component applications. Results of the experiments show that the techniques are viable.
Dokumenty
Stáhnout Dokument Autor Typ Velikost
Stáhnout Text práce RNDr. Pavel Parízek, Ph.D. 1.6 MB
Stáhnout Abstrakt v českém jazyce RNDr. Pavel Parízek, Ph.D. 80 kB
Stáhnout Abstrakt anglicky RNDr. Pavel Parízek, Ph.D. 81 kB
Stáhnout Posudek vedoucího prof. Ing. František Plášil, DrSc. 254 kB
Stáhnout Posudek oponenta Doc. RNDr. Ivana Černá, CSc. 207 kB
Stáhnout Posudek oponenta Prof. Corina Pasareanu 221 kB
Stáhnout Záznam o průběhu obhajoby 161 kB