[section]
MASARYKOVA UNIVERSITA
FAKULTA INFORMATIKY
SL
Grafická specifikace souběžných systémů
DIPLOMOVá PRáCE
David Šafránek
Brno, 2001
Prohlašuji, že tato práce je mým původním autorským dílem, které jsem vypracoval samostatně. Všechny zdroje, prameny a literaturu, které jsem při vypracování používal nebo z nich čerpal, v práci řádně cituji s uvedením úplného odkazu na příslušný zdroj.
Na tomto místě bych chtěl poděkovat zejména vedoucímu své diplomové práce doc. RNDr. Luboši Brimovi, CSc. za vedení a podnětné připomínky. Dále bych chtěl poděkovat členům laboratoře ParaDiSe za užitečné rady a podporu.
Shrnutí
Pro účely specifikace souběžných systémů byla vyvinuta řada textových specifikačních jazyků. Potřeba usnadnění a urychlení procesu specifikace vedla k zavedení grafických formalizmů. Podpora ze strany programových nástrojů však není zejména v případě tzv. koordinačních grafických jazyků, které jsou zaměřené na znázornění komunikačních vztahů mezi komponentami systému, v současné době dostatečná.
V práci je podrobně popsán jazyk GCCS (Graphical Calculus of Communicating Systems []). Byly uskutečněny pokusy o implementaci grafického editoru pro GCCS [] (později přepracováváno v rámci integrace do nástroje Concurrency Factory []). Implementace však nebyla dokončena a nebyla zveřejněna ani předběžná verze, zejména kvůli nestabilitě programu.
Součástí této práce je návrh a implementace editoru pro grafickou specifikaci souběžných systémů v tomto jazyce.
Práce obsahuje v teoretické části přehled nejznámějších grafických formalizmů a nástrojů pro specifikaci (příp. i verifikaci) souběžných systémů. Implementovaný editor jazyka GCCS zahrnuje podporu modulární a hierarchické specifikace systémů, inkrementální kontrolu konzistence grafické syntaxe a transformaci grafických GCCS specifikací do jazyka CCS. V rámci praktické části jsme provedli formální návrh algoritmu této transformace zachovávající původní sémantiku GCCS. Implementační část práce popisuje strukturu a použití implementovaného editoru. K implementaci jsme použili jazyk C++ a knihovnu Qt.
Klíčová slova
grafická specifikace souběžných systémů, specifikační jazyk, grafický jazyk, GCCS, CCS, koordinační model, koordinační jazyk