Hlavním cílem této diplomové práce je navrhnout a implementovat nástroj pro podporu grafické specifikace souběžných systémů s inkrementální kontrolou konzistence grafické syntaxe (na rozdíl od existujících nástrojů pro grafickou specifikaci Argonaute [], Auto/Graph []), který umožní export specifikovaných systémů do jazyka akceptovaného verifikačními nástroji.
V teoretické části práce uvedeme přehled grafických specifikačních formalizmů (kapitola 
), jež usnadňují specifikaci a popis souběžných systémů. Z těchto formalizmů jsme vybrali pro implementaci formální grafický jazyk GCCS (zavedený v článku []), zejména díky jeho vhodnosti pro modulární a hierarchickou specifikaci souběžných systémů a blízkému vztahu k algebře procesů CCS.
Jazyk GCCS byl původně navržen pro grafickou specifikaci systémů v komplexním verifikačním nástroji Concurrency Factory []. Součástí tohoto nástroje byla implementace grafického editoru GCCS [], program však nebyl dokončen k praktickému použití, zejména kvůli nestabilitě a nevyhovujícímu uživatelskému rozhraní. Grafický editor nebyl implementován objektově a nedisponoval vyhovujícím uživatelským rozhraním. Pro účely verifikace měl být grafický popis systému kompilován do přechodových systémů s návěštími. V době implementace tohoto editoru nebyl jazyk GCCS ještě formalizován, jednalo se o první pokus graficky specifikovat procesy CCS.
Součástí této práce je objektově orientovaná implementace editoru jazyka GCCS vycházející z formalizace jazyka uvedené v [] a dále rozvedené v kapitole v této práci. Při návrhu tohoto editoru jsme kladli důraz na jednoduchost jeho ovládání.
Praktická část obsahuje formální návrh algoritmu pro transformaci specifikací jazyka GCCS do kalkulu CCS a důkaz ekvivalence sémantiky transformovaného systému se sémantikou původní grafické reprezentace (kapitola ). V kapitole popíšeme implementovaný grafický editor a v kapitole , provedeme porovnání s podobnými známými editory a uvedeme příklad jeho použití.
Práci zakončíme závěrem poskytujícím shrnutí dosažených výsledků a motivaci k další práci.