Technical Reports
The report FIMU-RS-2009-10
Decidable Race Condition for HMSC
by
Vojtěch Řehák,
Petr Slovák,
Jan Strejček,
Loic Hélouet,
December 2009, 30 pages.
FIMU-RS-2009-10.
Available as Postscript,
PDF.
Abstract:
Races in Message Sequence Charts may lead to a bad interpretation of
described behaviours, and are often considered as a design error. While
there is a quadratic-time algorithm detecting races in Basic Message
Sequence Charts (BMSCs), the problem is undecidable for High-level
Message Sequence Charts (HMSCs). 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
(the problem is in P if the number of processes and gates is fixed).
