Decidable Race Condition and Open Coregions in HMSC - Rehak, Vojtech; Slovak, Petr; Strejcek, Jan; Helouet, Loic (Electronic Communications of the EASST, 2010)
Message Sequence Charts (MSCs) is a visual formalism for the description ofcommunication behaviour of distributed systems. An MSC specifies relationsbetween communication events with partial orders. A situation when twovisually ordered events may occur in any order during an execution of an MSCis called a race and is usually considered as a design error. While thereis a quadratic time algorithm detecting races in a finite communicationbehaviours called Basic Message Sequence Charts (BMSCs), the race detectionproblem is undecidable for High-level Message Sequence Charts (HMSCs), anMSC formalism describing potentially infinite sets of potentially unboundedbehaviours. To improve this negative situation for HMSCs, we introduce twonew notions: a new concept of race called trace-race and an extension of theHMSC formalism with open coregions, i.e. coregions that can extend over morethan one BMSC. We present three arguments showing benefits of our notionsover the standard notions of race and HMSC. First, every trace-race-freeHMSC is also race-free. Second, every race-free HMSC can be equivalentlyexpressed as a trace-race-free HMSC with open coregions. Last, thetrace-race detection problem for HMSC with open coregions is decidable andPSPACE-complete. Finally, the proposed extension of coregions allows torepresent in a visual fashion whether an arbitrary number of racing eventsin the usual MSC formalism are concurrent or not.