Abstract
Message Sequence Charts (MSCs) and High-level Message Sequence Charts (HMSC) are formalisms used to describe scenarios of message passing protocols. We propose using Allen’s logic to study the temporal order of the messages. We introduce the concept of discord to quantify the order discrepancies between messages in different nodes of an HMSC and study its algorithmic properties. We show that while discord of a pair of messages is hard to compute in general, the problem becomes polynomial-time computable if the number of nodes of the HMSC or the number of processes is constant. Moreover, for a given HMSC, it is always computationally easy to identify a pair of messages that exhibits the worst-case discord, and compute the discord of this pair.
Work partly supported by the ESF project Automatha and the ANR-06-SETI project DOTS.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Allen, J.F.: Maintaining Knowledge about Temporal Intervals. Communications of ACM 26(11), 832–843 (1983)
Alur, R., Holzmann, G., Peled, D.: An Analyzer for Message Sequence Charts. Software — Concepts and Tools 17, 70–77 (1996)
Alur, R., Etessami, K., Yannakakis, M.: Realizability and Verification of MSC Graphs. Theoretical Computer Science 331(1), 97–114 (2005)
Ben-Abdallah, H., Leue, S.: Syntactic 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)
Brand, D., Zafiropulo, P.: On Communicating Finite-State Machines. Journal of the ACM 30(2), 323–342 (1983)
Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design 19(1), 45–80 (2001)
Elkind, E., Genest, B., Peled, D.: Detecting Races in Ensembles of Message Sequence Charts. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, Springer, Heidelberg (2007)
Elkind, E., Genest, B., Peled, D., Spoletini, P.: Quantifying the Discord: Order Discrepancies in Message Sequence Charts, available from http://perso.crans.org/~genest/EGPS07.pdf
Floyd, R.W.: Algorithm 97 (Shortest Path). Communications of the ACM 356 (1962)
Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)
ITU Z120 standard recommendation (1996)
Krokhin, A., Jeavons, P., Jonsson, P.: Reasoning about Temporal Relations: The Tractable Subalgebras of Allen’s Interval Algebra. J. ACM 50(5), 591–640 (2003)
Lohrey, M., Muscholl, A.: Bounded MSC communication. Information and Computation 189, 160–181 (2004)
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)
Peled, D.: Specification and Verification of Message Sequence Charts. In: FORTE 2000, IFIP CP 183, pp. 139–154 (2000)
Warshall, S.: A Theorem on Boolean Matrices. Journal of the ACM 9(1), 11–12 (1962)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Elkind, E., Genest, B., Peled, D., Spoletini, P. (2007). Quantifying the Discord: Order Discrepancies in Message Sequence Charts. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds) Automated Technology for Verification and Analysis. ATVA 2007. Lecture Notes in Computer Science, vol 4762. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75596-8_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-75596-8_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75595-1
Online ISBN: 978-3-540-75596-8
eBook Packages: Computer ScienceComputer Science (R0)