Title
Detecting races in ensembles of message sequence charts
Abstract
The analysis of message sequence charts (MSCs) is highly important in preventing common problems in communication protocols. Detecting race conditions, i.e., possible discrepancies in event order, was studied for a single MSC and for MSC graphs (a graph where each node consists of a single MSC, also called HMSC). For the former case, this problem can be solved in quadratic time, while for the latter case it was shown to be undecidable. However, the prevailing real-life situation is that a collection of MSCs, called here an ensemble, describing the different possible scenarios of the system behavior, is provided, rather than a single MSC or an MSC graph. For an ensemble of MSCs, a potential race condition in one of its MSCs can be compensated by another MSC in which the events occur in a different order. We provide a polynomial algorithm for detecting races in an ensemble. On the other hand, we show that in order to prevent races, the size of an ensemble may have to grow exponentially with the number of messages. Also, we initiate the formal study of the standard MSC coregion construct, which is used to relax the order among events of a process. We show that by using this construct, we can provide more compact race-free ensembles; however, detecting races becomes NP-complete.
Year
DOI
Venue
2007
10.1007/978-3-540-71209-1_32
TACAS
Keywords
Field
DocType
former case,latter case,different possible scenario,different order,msc graph,event order,message sequence chart,detecting race condition,compact race-free ensemble,single msc,standard msc,communication protocol,race condition
Graph,Race condition,Computer science,Algorithm,Theoretical computer science,Polynomial algorithm,Time complexity,Exponential growth,Communications protocol,Undecidable problem
Conference
Volume
ISSN
Citations 
4424
0302-9743
3
PageRank 
References 
Authors
0.39
17
3
Name
Order
Citations
PageRank
Edith Elkind11340120.81
Blaise Genest230425.09
Doron Peled33357273.18