Fakulta informatiky MU
ANF DATA, spol. s r. o. Londýnské nám. 886/4 639 00 Brno
Mgr.  Radek Sedláček, Ph.D. • ANF DATA • Londýnské nám. 886/4 • 639 00 Brno
Pro:
studijní oddělení FI MU Brno
Mgr. Radek Sedláček, Ph.D. Sř: +420 538 776 880 Fax: +420 538 776 540
e-mail:
radek.sedlacekOsiemens.com
Věc:   Posudek oponenta na bakalářskou práci Luboše Ko-renčiaka Time Extension of Message Sequence Chart
17. 6. 2009
Předkládaná bakalářská práce se zabývá rozšířením formalismu MSC o časová omezení. Podává přehled existujících přístupů k tomuto rozšíření a definuje vlastní, tzv. proper časová omezení. Z existujících přístupů vybírá nejvhodnější k řešení těchto proper časových omezení a uvádí dva algoritmy pro řešení časových omezení v podobě intervalů a timerů. Dále se práce věnuje tzv. tightening MSC a výpočtu minimální sítě. Zde autor uvádí svůj vlastní přístup a zavádí několik operátorů potřebných k výpočtu. Uvádí algoritmus pro výpočet nad MSC a nastiňuje i možnost, jak řešit tento problém pro MSC Text práce sestává ze 40 stran včetně obsahu a seznamu literatury, logicky je členěn do osmi kapitol.
Hodnocení práce
Jazykově je práce psána velmi čistě, i když občasným překlepům se autor nevyhnul. Například na straně 13 se píše For a the formal definition of the tightening we have to define a solution set. V žádném případě ovšem tyto prohřešky nebrání porozumění textu. Typografické chyby jsem v práci také nenalezl, reference na použité zdroje jsou uváděny správně a seznam použitých zdrojů na konci práce se také zdá být úplný.
Struktura práce je čitelná, každá podkapitola začíná popisem toho, co čtenář může dále v textu příslušné podkapitoly nalézt. K úvodní kapitole nemám připomínek.
V kapitole druhé lze nalézt základní formální definice MSC, HMSC a MSCG. Oceňuji stručnost a výstižnost kapitoly, jsou uvedeny skutečně jen ty definice, se kterými se dále v práci operuje.
Kapitola třetí se zabývá rozšířením MSC o časová omezení, obsahuje nejdříve nutné formální definice časových omezení a o ně rozšířených MSC a MSG, dále se definuje tzv. časově konzistentní MSC a MSG. Dalšími definicemi jsou množiny řešení pro MSC a MSG, minimální MSC/MSG a problém nalezení minimální sítě MSC/MSG. Na závěr kapitoly, a to je třeba ocenit, si autor stanovuje kritéria, která musí splňovat přístup použitý k řešení tohoto problému.
Ve čtvrté kapitole autor srovnává různé přístupy k řešení problému časových omezení a výpočtu minimální sítě. Z textu je zřejmé, že autor prostudoval spoustu dosud publikovaných prací o této problematice a dokazuje, že byl schopen se v teoretických pracích dobře zorientovat a na základě vlastních kritérií zvolit nejvhodnější přístup, kterým je struktura nazývaná labeled partially ordered set. Na závěr autor zdůrazňuje, že ani tento přístup neřeší zcela všechny problémy svázané s časovými omezeními.
V  páté kapitole autor zavádí definici tzv. proper časových omezení. Snahou přitom je definovat taková omezení, která by nebyla nejednoznačná. Jádrem kapitoly jsou pak dva algoritmy pro ověření, zda časová omezení v MSG jsou proper. Nechybí ani rozbor korektnosti obou algoritmů, což je chvályhodné a je vidět, že autor přistoupil i k algoritmické části práce velmi zodpovědně. Zároveň uvádí i jejich možnou optimalizaci.
Šestá kapitola pojednává o nalezení minimální sítě v MSC. Po nutném zavedení nových operátorů přicházejí na řadu dva teorémy i s důkazy. Je patrné, že práce s formálním aparátem, větami a důkazy nečiní autorovi žádné potíže. Ačkoliv nejsem schopen při zběžném přečtení důkazů ověřit jejich korektnost, nenašel jsem v nich na první pohled zjevnou chybu.
Sedmá kapitola je věnována nalezení minimální sítě pro MSG, kde hlavním problémem jsou cykly v grafu, což autor správně shrnuje posledním dokázaným teorémem.
V  závěrečné kapitole práce autor zcela upřímně shrnuje dosažené výsledky a nastiňuje směry budoucího teoretického vývoje i návrh svoje výsledky implementovat v nástroji SCstudio.
Vzhledem k velmi zdařilé kompozici práce, která jasně dává smysl a je z ní vidět, odkud kam směřuje a co přináší nového na poli teorie časových omezení MSC, navrhuji práci přepsat do podoby článku a ten poslat na vhodnou vědeckou konferenci. Svým rozsahem a kvalitou zcela jistě předložená práce splnila zadání a dokonce přesáhla požadavky kladené na bakalářskou práci, proto ji navrhuji přijmout k obhajobě a ohodnotit známkou A.
Obhajoby se osobně zúčastním.
Mgr. Radek Sedláček, Ph.D.