next up previous contents
Next: Další možné přístupy Up: Jazyky vycházející z koordinačních modelů Previous: Vlastnosti grafických koordinačních jazyků

Grafické koordinační jazyky a dostupné nástroje

Formálních grafických koordinačních jazyků určených pro specifikaci souběžných systémů nebylo zatím mnoho vyvinuto. V dalších kapitolách této práce se zabýváme jazykem GCCS [], který spadá do této kategorie. Pro jazyk GCCS zatím neexistuje použitelný editační a verifikační nástroj. Proto je součástí této práce implementace grafického editoru pro GCCS umožňujícího verifikaci prostřednictvím nástroje The Concurrency Workbench of New Century [].

V rámci projektu Meije při INRIA Sophia Antipolis byl vyvinut balík verifikačních nástrojů Auto/Graph [], který obsahuje editor pro grafickou specifikaci systémů. Podporovaný grafický jazyk však není formální, kontrola konzistence specifikace je prováděna až při překladu do meziformátu FC2 pro popis synchronizujících konečných přechodových systémů. Tyto specifikace lze pak verifikovat pomocí nástrojů FC2TOOLS. Jak ukazují obrázky gif a gif v předchozí sekci, tento nástroj podporuje hierarchický a modulární popis systémů. Grafický editor nedisponuje uživatelsky příjemným rozhraním pro jeho ovládání, praktické použití tohoto editoru je složité.

Dalším grafickým jazykem vycházejícím z principů koordinačních jazyků je jazyk DART []. Jeho sémantika je definována transformací grafických specifikací do jazyka LOTOS []. Sémantika jazyka LOTOS je kompoziční, což zaručuje hierarchii a modulárnost jazyka DART. Pro jazyk DART byl implementován grafický editor GLD. Jeho nevýhodou je provádění kontroly konzistence specifikace stejně jako u předchozího nástroje až při překladu do cílového textového jazyka (v tomto případě LOTOS). Nástroj GLD již není dále vyvíjen.

Zajímavým nástrojem pro grafickou specifikaci distribuovaných systémů je Autofocus []. Tento nástroj podporuje několik různých přístupů specifikace a popisu. Jeho součástí je formalizmus pro popis koordinačních vztahů komponent v hierarchickém smyslu vycházející z diagramů toku dat, stavové diagramy pro popis chování komponent a formalizmus pro alternativní popis sekvencí událostí podobný Message Sequence Charts (viz následující sekce). Tyto grafické formalizmy jsou kombinovány s textovým jazykem pro popis datových typů komunikačních kanálů a lokálních proměnných jednotlivých komponent. Nástroj neumožňuje export specifikací do jiných formalizmů, čímž jsou možnosti verifikace omezeny jen na vlastní možnosti nástroje. Verifikační techniky však zatím nejsou implementovány.


next up previous contents
Next: Další možné přístupy Up: Jazyky vycházející z koordinačních modelů Previous: Vlastnosti grafických koordinačních jazyků

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