velikost textu

Behavior Protocols Extensions

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:
Behavior Protocols Extensions
Typ:
Disertační práce
Autor:
RNDr. Jan Kofroň, Ph.D.
Školitel:
prof. Ing. František Plášil, DrSc.
Oponenti:
doc. Ing. Karel Richta, CSc.
prof. Dr. Uwe Assmann
Id práce:
40903
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 (I2)
Přidělovaný titul:
Ph.D.
Datum obhajoby:
24. 9. 2007
Výsledek obhajoby:
Prospěl/a
Jazyk práce:
Angličtina
Abstract v angličtině:
Formal verification of behavior of a component application requires a suitable specification language. It is necessary that the specification language captures all important aspects of the future implementation with respect to desired properties. Behavior Protocols have been proven to be a suitable component behavior specification platform if one is interested in absence of communication errors. In this thesis, we (1) propose a new specification language based on Behavior Protocols and (2) address the issue of insufficient performance of BPChecker—a proprietary tool for verification of absence of communication errors in Behavior Protocols. Motivated by issues raised during specification of a real-life-sized case study aiming at providing wireless Internet access at airports, we extended the original Behavior Protocols with support for method parameters, local variables, synchronization of more than two components, and specification of variable-controlled loops. To address the second issue, we propose a method for verification of Behavior Protocols via their transformation to Promela—the input language of the Spin model checker.
Dokumenty
Stáhnout Dokument Autor Typ Velikost
Stáhnout Text práce RNDr. Jan Kofroň, Ph.D. 1.02 MB
Stáhnout Abstrakt v českém jazyce RNDr. Jan Kofroň, Ph.D. 80 kB
Stáhnout Abstrakt anglicky RNDr. Jan Kofroň, Ph.D. 80 kB
Stáhnout Posudek vedoucího prof. Ing. František Plášil, DrSc. 248 kB
Stáhnout Posudek oponenta doc. Ing. Karel Richta, CSc. 245 kB
Stáhnout Posudek oponenta prof. Dr. Uwe Assmann 313 kB
Stáhnout Záznam o průběhu obhajoby 200 kB