Posudek vedoucího na bakalářskou práci
Studentka: Eva Tesařová
Název práce: Modelování systémů s reálným časem a pravdě­
podobností
Cílem předložené bakalářské práce bylo zpracovat přehled modelovacích formalismů
pro modelování systémů s reálným časem a pravděpodobností a
vybraný formalismus časových pravděpodobnostních automatů rozšířit o
možnost specifikace diskrétní nespojité pravděpodobnostní distribuce definované
nad lokací automatu, která popisuje pravděpodobnost opuštění lokace
v daném čase. Tj. jakási diskrétní konečná aproximace principu C T M C
(Continuous-Time Markov Chains). Zadání práce nepožadovalo žádnou implementační
validaci navrženého rozšíření.
Text předložené práce bez výhrad naplňuje zadání. Zpracování tématu je
vynikající a jednoznačně prokazuje, že studentka má netriviální schopnosti
práce s formálními aparáty. Přehledová část práce není jen „tupým opisem"
dostupné literatury, ale je rozšířena o drobné komentáře a vlastní příklady,
které čtenáře provedou a upozorní na případná obtížně uchopitelná místa.
Má jediná drobná výtka je k absenci uceleného porovnání existujících formalismů
na jednom místě (veškeré informace v práci obsažené jsou, jen je
chtělo shrnout v obšírnější podobě třeba v závěru práce).
Otázky k obhajobě:
• Který z modelovacích jazyků dotčených verifikačních nástrojů byste
doporučila rozšířit tak, aby sledoval Vámi navržené konzervativní
rozšíření PTA, a jak konkrétně by rozšíření vypadalo?
Celkově hodnotím tuto bakalářskou práci jako bezproblémovou. Navrhuji
předloženou práci uznat jako práci bakalářskou a hodnotit ji stupněm
výborně (A). Věřím že při doplnění o vhodnou případovou studii, je obsah
práce publikovatelný v podobě odborného vědeckého článku.
V Brně dne 28. května 2014,
doc. RNDr. Jiří Barnat, Ph.D.