Příloha 6: Posudek oponenta habilitační práce
Masarykova univerzita Fakulta
Habilitační obor
Fakulta informatiky MU Informatika
Uchazeč Pracoviště Habilitační práce
RNDr. Jiří Barnat, Ph.D.
Fakulta informatiky, Masarykova univerzita
Platform-Dependent Verification
Oponent Pracoviště
doc. Ing. Tomáš Vojnar, Ph.D.
Fakulta informačních technologií, Vysoké učení technické v Brně
Text posudku (rozsah dle zvážení oponenta)
Habilitační práce RNDr. Jiřího Barnata, Ph.D. pokrývá významnou část jeho výzkumu v oblasti automatické formální verifikace založené na tzv. model chcekingu. Práce má charakter souboru uveřejněných vědeckých prací doplněných komentářem.
Oblast automatické verifikace je velmi živá, přitahuje zájem řady akademických i průmyslových pracovišť a je značně kompetitivní. Jedním z klíčových problémů, které se v této oblasti řeší, je problematika vyrovnávání se s tzv. stavovou explozí, tedy s exponenciálním nárůstem počtu stavů verifikovaných systémů v závislosti na velikosti zdrojového popisu těchto systémů. Právě do této oblasti spadají originální výzkumné výsledky dr. Barnata, které jsou součástí jeho habilitační práce. Všechny tyto výsledky se obecně zaměřují na inteligentní využití výpočetních zdrojů dostupných v moderních počítačových systémech.
První skupina výsledků dr. Barnata zahrnutá do habilitační práce se konkrétně týká distribuované implementace model cheekingu pro lineární temporální logiku (LTL), paralelní implementace LTL model cheekingu na architekturách se sdílenou pamětí a dále LTL model cheekingu s využitím grafických procesorů. Ve všech těchto oblastech dosáhl dr. Barnat spolu se svými spolupracovníky významných výsledků. Zvláště lze zmínit např. návrh implementačních technik umožňujících škálovatelný paralelní LTL model cheeking na paralelních architekturách se sdílenou pamětí, návrh lineárního algoritmu pro paralelní model cheeking významné podtřídy LTL vlastností umožňující ověřování zadané vlastnosti v průběhu generování stavového prostoru (tzv. on-the-fly model cheeking) či algoritmus pro detekci akceptujících cyklů, který je základním kamenem LTL model chcekingu, pro prostředí grafických procesorů.
Další skupina výsledků presentovaných v habilitační práci se týká efektivního využití diskové paměti v LTL model cheekingu. Z těchto výsledků si dle mého názoru zaslouží zvláště vyzdvihnout návrh algoritmu pro LTL model cheeking umožňující efektivní komunikaci s diskem a pracující v lineárním prostoru, který významně posunul možnosti do té doby existujících řešení. Tento výsledek byl publikován na prestižní konferenci CAV 2007. Jiným významným výsledkem z této oblasti je pak práce publikovaná na konferenci TACAS 2008, jež popisuje nový, v praxi výrazně efektivnější přístup k detekci již jednou nalezených stavů v rámci LTL model cheekingu využívajícího diskový prostor.
Třetí oblastí, která je v rámci habilitační práce pokryta, je oblast paralelní dekompozice grafů na silnč souvislé komponenty, což je operace, která je základem řešení mnoha problémů (nejen) v oblasti model cheekingu. Do této části habilitační práce je zahrnuta
dvojice navzájem navazujících výsledků vedoucí ktzv. rckursivnímu OBF algoritmu, který podle důkladného experimentálního vyhodnocení dr. Barnatem a jeho spoluautory překonává ve většině případů všechny ostatní známé algoritmy pro řešení daného problému.
Čtvrtá skupina výsledků presentovaná v rámci habilitační práce se týká paralelního kvantitativního LTL model cheekingu a dále kvantitativního model cheekingu systémů s degradací. V rámci první ze zmíněných oblastí je prezentováno nové, paralelní řešení lokálního kvantitativního model cheekingu pravděpodobnostních systémů, které umožnilo v některých provedených experimentech snížit spotřebu času z řádu dnů na řád minut.
Konečně pátá část presentovaných výsledků se týká nástrojů pro LTL model cheeking v distribuovaném a paralelním prostředí, na jejichž vývoji se dr. Barnat různým způsobem podílel. V této oblasti si vyzdvižení zaslouží to, že všechny presentované nástroje byly dovedeny do opravdu funkční podoby, umožňující aplikaci těchto nástrojů i lidmi mimo skupinu obklopující dr. Barnata, což nebývá u výzkumných prototypů vždy běžné. Úsilí investované do vývoje zmíněných nástrojů je zřejmě velmi velké, výraznč ovšem přispívá k rozvoji výzkumu v dané oblasti a také k aplikovatelnosti dosažených výsledků. Zmiňované nástroje jsou přitom s ohledem na svou funkcionalitu unikátní v mezinárodním měřítku.
Souhrnně lze říci, že odborná úroveň výsledků shrnutých v habilitační práci je velmi vysoká. Zmíněné výsledky byly presentovány na významných mezinárodních konferencích (představujících v oblasti informatiky dle mého názoru stále primární publikační fórum), na solidních mezinárodních workshopech i v mezinárodních vědeckých časopisech. Podíl dr. Barnata na presentovaných výsledcích je přiměřený. Význam presentovaných výsledků dokládá mj. řada jejich citací v mezinárodní vědecké literatuře. Z účasti řady doktorských studentů na uvedených publikacích je zřejmé, že dr. Barnat je významně zapojený do jejich přípravy. Positivně také hodnotím to, že na řadě z uvedených prací se podíleli výzkumníci z významných zahraničních výzkumných center, což dokladuje skutečnost, že dr. Barnat je výzkumníkem etablovaným na mezinárodní úrovni. Dále si myslím zaslouží ocenění i to, že výsledky dosažené dr. Barnatem jsou obvykle doprovázeny rozsáhlým experimentálním vyhodnocením a navíc jsou základem propracovaných nástrojů zveřejněných všem zájemcům na Internetu.
Dotazy oponenta k obhajobě habilitační práce (počet dotazů dle zvážení oponenta)
Zabýval jste se kombinací Vámi navržených přístupů využívajících výpočetní sílu moderních výpočetních systémů s jinými přístupy k vyrovnávání se se stavovou explozí, zejména pak s technikami redukce stavových prostorů? Jaké jsou zkušenosti s takovými kombinacemi?
Habilitační práce Jiřího Barnata „Platform-Dependent Verification'' splňuje požadavky standardně kladené na habilitační práce v oboru Informatika.
Závěr
/
Brno, 21.2.2011
doc. Ing. Tomáš Vojnar, Ph.D.