Decidable Race Condition and Open Coregions in HMSC

Logo poskytovatele
Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Rozhodnutelné podmínky souběhu a otevřené koregiony v HMSC
Autoři

ŘEHÁK Vojtěch SLOVÁK Petr STREJČEK Jan HÉLOUËT Loic

Rok publikování 2010
Druh Článek ve sborníku
Konference Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://journal.ub.tu-berlin.de/index.php/eceasst/issue/view/39
Obor Informatika
Klíčová slova HMSC; race condition; trace-race condition; open coregions;
Popis Message Sequence Charts (MSCs) je vizuální formalizmus pro popis komunikačních chování distribuovaných systémů. MSC specifikuje vztahy částečného uspořádání mezi komunikačními událostmi. Situace, kdy dvě vizuálně uspořádané události se mohou při průběhu implementace MSC udát v opačném pořadí, se nazývá souběh (race) a je obvykle považována za chybu návrhu. Přestože pro popisy konečných chování (BMSC) je rozhodování problému řešitelné v kvadratickém čase, problém souběhu je nerozhodnutelný pro HMSC (MSC formalizmus pro potenciálně nekonečné množiny neomezených chování. Pro vylepšení této negativní situace pro HMSC zavádíme dva nové koncepty: stopový souběh a otevřené koregiony. Ukazujeme trojí přínos našeho přístupu. Za prvé každé HMCS bez stopového souběhu je i bez souběhu. Za druhé každé HMSC bez souběhu může být ekvivalentně vyjádřeno i jako HMCS bez stopového souběhu s využitím otevřených koregionů. Za třetí problém detekce stopových souběhů v HMSC s otevřenými koregiony je rozhodnutelný a PSPACE-úplný.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info