Systems Biology Laboratory Faculty of Informatics, Masaryk University
Botanická 68a, 602 00 Brno, Czech Republic
Phone: (+420) 549 493 647 Fax:        (+420) 549 491 820
From: Prof. RNDr. Luboš Brim, CSc. Head of the Laboratory
e-mail: brim@fi.muni.cz
POSUDEK TEZI DISERTAČNÍ PRACE
Autor:   Mgr. Jana Tůmová
Název:    Quantitative Linear-Time Model Checking
Automatizovaná formální verifikace, zejména metoda ověřování modelu (model checking), je stále častěji akceptována průmyslovou praxí nejen jako jedna z dominantních technik pro zvýšení kvality výpočetních systémů, ale také jako metoda pro snížení nákladů a zrychlení vývoje těchto systémů. Model checking je tradičně spojován s analýzou kvalitativních vlastností systémů, vyjadřovaných zpravidla jako formule temporální logiky. V řadě aplikací je však nezbytné verifikovat i vlastnosti, které mají kvantitativní charakter. Příkladem jsou kvantitativní časové vlastnosti nebo pravděpodobnostní vlastnosti chování systému.
Oblast kvantitativní analýzy je významná a je v současné době intenzivně rozvíjenou oblastí formální verifikace s řadou teoreticky i prakticky velmi zajímavých problémů. Jedním z klíčových je možnost využít lineární temporální logiku k verifikaci kvantitativních vlastností. Tento problém je tématem zamýšlené disertační práce.
V úvodní části předložených tezí disertační práce autorka identifikuje dva hlavní úkoly, kterým se chce věnovat. Prvním je LTL model checking pro systémy s degradací, které umožnňují zachytit zajímavé kvantitativní vlastnosti systémů. Druhým úkolem je problém syntézy řídící jednotky (controller synthesis) pro systémy s degradací.
V další části tezí autorka podává přehled současného stavu poznaní v dané oblasti. Vedle popisu známých přístupů se věnuje svému vlastnímu přínosu do problematiky kvantitativní analýzy. Rovněž shrnuje hlavní otevřené problémy. V závěru tezí je uvedeno zamýšlené zaměření disertační práce, předpokládané výsledky a časový harmonogram.
Téze jsou psány ve velmi dobré angličtině, text je ve své podstatě výborným stručným úvodem do problematiky. Výstižně postihuje hlavní problémy a do jejich kontextu zasazuje předpokládaný směr výzkumu autorky. Tezím nelze nic zásadního vytknout.
Závěrem mohu konstatovat, že navržená disertační práce má jasně stanovené cíle, které jsou ambicózní a bezesporu dizertabilní. Jejich dosažení je reálné v navrženém termínu. O tom, že autorka je na dobré cestě svědčí již publikované kvalitní výsledky.
V Brně 20. dubna 2010
prof. RNDr. Luboš Brim, CSc.