Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{878519,
author = {Řehák, Vojtěch and Slovák, Petr and Strejček, Jan and Hélouët, Loïc},
address = {Paphos, Kypr},
booktitle = {Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010)},
editor = {Jochen Küster, Emilio Tuosto},
keywords = {HMSC; race condition; trace-race condition; open coregions;},
language = {eng},
location = {Paphos, Kypr},
publisher = {ECEASST},
title = {Decidable Race Condition and Open Coregions in HMSC},
url = {http://journal.ub.tu-berlin.de/index.php/eceasst/issue/view/39},
year = {2010}
}
TY - JOUR
ID - 878519
AU - Řehák, Vojtěch - Slovák, Petr - Strejček, Jan - Hélouët, Loïc
PY - 2010
TI - Decidable Race Condition and Open Coregions in HMSC
PB - ECEASST
CY - Paphos, Kypr
KW - HMSC
KW - race condition
KW - trace-race condition
KW - open coregions;
UR - http://journal.ub.tu-berlin.de/index.php/eceasst/issue/view/39
N2 - 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.
ER -
ŘEHÁK, Vojtěch, Petr SLOVÁK, Jan STREJČEK a Loïc HÉLOU$\backslash$''ET. Decidable Race Condition and Open Coregions in HMSC. In Jochen Küster, Emilio Tuosto. \textit{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.
|
