Decidable Race Condition and Open Coregions in HMSC
ŘEHÁK, Vojtěch, Petr SLOVÁK, Jan STREJČEK a Loïc HÉLOUËT. Decidable Race Condition and Open Coregions in HMSC. In Jochen Küster, Emilio Tuosto. Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010). Paphos, Kypr: ECEASST, 2010, 12 s. ISSN 1863-2122. |
Další formáty:
BibTeX
LaTeX
RIS
|
Základní údaje | |
---|---|
Originální název | Decidable Race Condition and Open Coregions in HMSC |
Název česky | Rozhodnutelné podmínky souběhu a otevřené koregiony v HMSC |
Autoři | ŘEHÁK, Vojtěch (203 Česká republika, garant, domácí), Petr SLOVÁK (203 Česká republika), Jan STREJČEK (203 Česká republika, domácí) a Loïc HÉLOUËT (250 Francie). |
Vydání | Paphos, Kypr, Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010), 12 s. 2010. |
Nakladatel | ECEASST |
Další údaje | |
---|---|
Originální jazyk | angličtina |
Typ výsledku | Stať ve sborníku |
Obor | 10201 Computer sciences, information science, bioinformatics |
Stát vydavatele | Kypr |
Utajení | není předmětem státního či obchodního tajemství |
WWW | URL |
Kód RIV | RIV/00216224:14330/10:00043646 |
Organizační jednotka | Fakulta informatiky |
ISSN | 1863-2122 |
Klíčová slova česky | HMSC; podmínky souběhu; stopové podmínky souběhu; otevřené koregiony; |
Klíčová slova anglicky | HMSC; race condition; trace-race condition; open coregions; |
Štítky | Message Sequence Charts, Network protocol description, race condition checking, race conditions |
Příznaky | Mezinárodní význam, Recenzováno |
Změnil | Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 28. 4. 2011 15:15. |
Anotace |
---|
Message Sequence Charts (MSCs) is a visual formalism for the description of communication behaviour of distributed systems. An MSC specifies relations between communication events with partial orders. A situation when two visually ordered events may occur in any order during an execution of an MSC is called a race and is usually considered as a design error. While there is a quadratic time algorithm detecting races in a finite communication behaviours called Basic Message Sequence Charts (BMSCs), the race detection problem is undecidable for High-level Message Sequence Charts (HMSCs), an MSC formalism describing potentially infinite sets of potentially unbounded behaviours. To improve this negative situation for HMSCs, we introduce two new notions: a new concept of race called trace-race and an extension of the HMSC formalism with open coregions, i.e. coregions that can extend over more than one BMSC. We present three arguments showing benefits of our notions over the standard notions of race and HMSC. First, every trace-race-free HMSC is also race-free. Second, every race-free HMSC can be equivalently expressed as a trace-race-free HMSC with open coregions. Last, the trace-race detection problem for HMSC with open coregions is decidable and PSPACE-complete. Finally, the proposed extension of coregions allows to represent in a visual fashion whether an arbitrary number of racing events in the usual MSC formalism are concurrent or not. |
Anotace česky |
---|
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ý. |
Návaznosti | |
---|---|
GAP202/10/1469, projekt VaV | Název: Formální metody pro analýzu a verifikaci komplexních systémů |
Investor: Grantová agentura ČR, Formální metody pro analýzu a verifikaci komplexních systémů | |
GP201/08/P375, projekt VaV | Název: Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik |
Investor: Grantová agentura ČR, Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik | |
GP201/08/P459, projekt VaV | Název: Nové možnosti automatické verifikace síťových protokolů |
Investor: Grantová agentura ČR, Nové možnosti automatické verifikace síťových protokolů | |
MSM0021622419, záměr | Název: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy | |
MUNI/A/0914/2009, interní kód MU | Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV) |
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty | |
1M0545, projekt VaV | Název: Institut Teoretické Informatiky |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky |
VytisknoutZobrazeno: 19. 9. 2024 09:40