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.
Chapter PDF
References
Alur, R., Etessami, K., Yannakakis, M.: Inference of message sequence charts. IEEE Transactions on Software Engineering 29, 623–633 (2003)
Alur, R., Holzmann, G., Peled, D.: An analyzer for message sequence charts. Software Concepts and Tools 17(2), 70–77 (1996)
Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 114–129. Springer, Heidelberg (1999)
Ben-Abdulla, H., Leue, S.: Symbolic detection of process divergence and non-local choice in message sequence charts. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 259–274. Springer, Heidelberg (1997)
Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Formal Methods in System Design 19, 45–80 (2001)
Hélouët, L., Jard, C.: Conditions for synthesis of communicating automata from HMSCs. In: 5th International Workshop on Formal Methods for Industrial Critical Systems (2000)
Holzmann, G., Peled, D., Redberg, M.: Design tools for requirements engineering. Bell Labs Technical Journal 2, 86–95 (1997)
ITU-T Recommendation Z.120, Message Sequence Chart (MSC), Geneva (1996)
Krueger, I.: Distributed system design with message sequence charts. Ph.D. Thesis, TU Munchen (2000)
Kuske, D.: Regular sets of infinite message sequence charts. Information and Computation 187, 80–109 (2003)
Lohrey, M.: Safe realizability of high-level message sequence charts. In: Brim, L., et al. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 177–192. Springer, Heidelberg (2002)
Madhusudan, P.: Reasoning about sequential and branching behaviours of message sequence graphs. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 809–820. Springer, Heidelberg (2001)
Mukund, M., Narayan Kumar, K., Sohoni, M.: Synthesizing distributed finite-state systems from MSCs. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 521–535. Springer, Heidelberg (2000)
Muscholl, A., Peled, D.: Message sequence graphs and decision problems on Mazurkiewicz traces. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 81–91. Springer, Heidelberg (1999)
Muscholl, A., Peled, D., Su, Z.: Deciding properties of message sequence charts. In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998. LNCS, vol. 1378, pp. 226–242. Springer, Heidelberg (1998)
Sengupta, B., Cleaveland, R.: Triggered message sequence charts. IEEE TSE (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Elkind, E., Genest, B., Peled, D. (2007). Detecting Races in Ensembles of Message Sequence Charts. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)