next up previous contents
Next: Motivace k další práci Up: Implementační část Previous: Uložení projektu a transformace

Závěr

V teoretické části tato práce podala přehled nejznámějších formalizmů a nástrojů pro hierarchickou grafickou specifikaci souběžných systémů. Ukázalo se, že většina grafických formalizmů s vyhovující podporou editačních nástrojů je určena pro specifikaci reaktivních systémů a systémů reálného času. Tyto formalizmy však většinou nepodporují modulární specifikaci, nejsou tedy vhodné pro specifikaci systémů, u nichž je klíčové přehledné vyjádření komunikačních vztahů jednotlivých komponent.

Naopak grafické koordinační jazyky, které modulární specifikaci umožňují, nemají dostatečnou podporu editačních nástrojů. Z těchto formalizmů jsme vybrali jazyk GCCS, který jsme podrobně rozebrali, dále rozvedli jeho formalizaci uvedenou v [] a provedli drobné úpravy v jeho definici. Pro upravenou verzi jazyka GCCS jsme navrhli a implementovali grafický editor umožňující transformaci grafických specifikací souběžných systémů do kódu CCS podporovaného verifikačním nástrojem The Concurrency Workbench of New Century []. Provedli jsme formální návrh, důkaz sémantické korektnosti a implementaci algoritmu této transformace.

Implementovaný editor GCCS podporuje hierarchickou a modulární specifikaci. Na rozdíl od prvního neúspěšného pokusu o implementaci editoru pro tento jazyk [] (součást []) jsme vytvořili objektově orientovaný snadno rozšiřitelný program disponující flexibilnějším uživatelským rozhraním. Oproti známým dostupným nástrojům, které využívají koordinačních jazyků ke specifikaci systémů, podporuje námi implementovaný editor inkrementální kontrolu konzistence grafických specifikací.





David Safranek
Fri Apr 6 23:53:25 MET DST 2001