Decidable Race Condition and Open Coregions in HMSC
Název česky | Rozhodnutelné podmínky souběhu a otevřené koregiony v HMSC |
---|---|
Autoři | |
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 | |
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: |
|