velikost textu

Automated verification of software

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:
Automated verification of software
Název v češtině:
Automatická veri kace software
Typ:
Disertační práce
Autor:
RNDr. Ondřej Šerý, Ph.D.
Školitel:
prof. Ing. František Plášil, DrSc.
Oponenti:
doc. Ing. Jan Janeček, CSc.
Carlo Ghezzi
Id práce:
44451
Fakulta:
Matematicko-fyzikální fakulta (MFF)
Pracoviště:
Katedra distribuovaných a spolehlivých systémů (32-KDSS)
Program studia:
Informatika (P1801)
Obor studia:
Softwarové systémy (4I2)
Přidělovaný titul:
Ph.D.
Datum obhajoby:
24. 9. 2010
Výsledek obhajoby:
Prospěl/a
Jazyk práce:
Angličtina
Abstrakt:
Přes výzkumné usilí věnované automatické verikaci software, její pronikání do softwarového průmyslu je stále spíše pomalé. Toto váhání mělo několik důvodů 1) složitost posouzení jednotlivých nástrojů, 2) složitost použití nástrojů a jejich integrace do vvývojového procesu. Pro usnadnění výběru jednotlivých nástrojů je součástí práce přehled technik založených na model checkingu kódu s porovnáním technik na základě jednotných kritérií. Navíc práce obsahuje průmyslovou případovou studii používající model checker BLAST. K posouzení vhodnosti nástrojů je potřeba i odpovovídajícího vzdělání, přikládáme tedy i své zkušenosti s přípravou dvou magisterských přednášek o formálních metodách. Integrací snadno použitelného specikačního jazyka do model checkeru BLAST, přispíváme k usnadnění použití tohoto nástroje. Mimo to představujeme koncept unit checkingu, tedy kombinace unit testingu a model checkingu kódu. Unit checking pomáhá s integrací model checkingu kódu do vývojového procesu.
Abstract v angličtině:
Despite the research eort being invested into the eld of automated verication of software, its adoption in industry is still rather slow. Several reasons for this hesitation may be identied. The thesis focuses on the following two (i) dificulty of assessment of dierent tools, and (ii) difficulty of tools usage and integration in the development process. To facilitate tool assessment, we provide a comprehensive overview of code model checking techniques with evaluation based on a common set of criteria. In addition, we contribute by an industrial case study on applicability of the BLAST model checker. Since also proper education is necessary for the ability of tool assessment, we include our experience report on preparation of two master-level formal method courses. By incorporating an easy to use specication language into the BLAST model checker, the thesis contributes to facilitating tools usage. In addition, we introduce the concept of unit checking, a combination of unit testing and code model checking, which helps integration of code model checking in the software development process.
Dokumenty
Stáhnout Dokument Autor Typ Velikost
Stáhnout Text práce RNDr. Ondřej Šerý, Ph.D. 3.22 MB
Stáhnout Abstrakt v českém jazyce RNDr. Ondřej Šerý, Ph.D. 80 kB
Stáhnout Abstrakt anglicky RNDr. Ondřej Šerý, Ph.D. 80 kB
Stáhnout Posudek vedoucího prof. Ing. František Plášil, DrSc. 47 kB
Stáhnout Posudek oponenta doc. Ing. Jan Janeček, CSc. 75 kB
Stáhnout Posudek oponenta Carlo Ghezzi 90 kB
Stáhnout Záznam o průběhu obhajoby 62 kB