next up previous contents
Next: Jazyk CCS Up: Praktická část Previous: Praktická část

Korespondence GCCS a CCS

  

V předchozí kapitole jsme uvedli sémantiku GCCS pomocí přechodových systémů s návěštími. Alternativně by bylo možné definovat sémantiku GCCS transformací do algebry procesů CCS. Tímto způsobem definice sémantiky GCCS bychom ztratili spojení mezi grafickou syntaxí a jejím významem, neboť případné nekonzistence v grafické specifikaci by byly odhaleny až při sémantickém zpracování příslušného CCS výrazu. Tuto chybu by nebylo možné ukázat v GCCS verzi specifikace. Pokud navíc požadujeme grafickou simulaci GCCS specifikací, přímá sémantika zaručuje její rychlejší odezvu.

Motivace pro transformaci GCCS systémů do kalkulu CCS spočívá v existenci dostupných verifikačních nástrojů pro tento formalizmus (zejména The Concurrency Workbench [] a []). Princip transformace je uveden v [], kde se však neuvažuje formální sémantika GCCS uvedená v předchozí kapitole (neboť v době psaní citované práce nebyl jazyk GCCS formalizován).

Naším cílem v této kapitole je formálně navrhnout algoritmus, který pro každý dobře definovaný GCCS systém vypočítá jemu sémanticky ekvivalentní CCS výraz a dokázat, že jím definovaná transformace zachovává sémantiku uvedenou v předchozí kapitole.

V závěru kapitoly pak naznačíme problémy opačného směru transformace, tedy transformace CCS výrazů na GCCS systémy.





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