Multiple Synchrony in MSC
Pages 149 - 166
Abstract
We propose an extension to Message Sequence Charts (MSC); MSC diagrams comprise processes (called instances) and messages. Messages in MSC are either asynchronous or method calls. Our extension adds multiple synchronous messages. We present a transformation algorithm that takes as input a diagram in the extended MSC and generates an equivalent one in the standard MSC. The synchronous messages are transformed to the standard notation via the introduction of several control messages. We also define a semantics for MSC (both the standard and our extension) using the process algebra CSP. Both instances and messages in MSC are characterised as CSP processes. This semantics allows us to formally establish the equivalence between an extended MSC diagram and its corresponding standard diagram (generated by the transformation algorithm). Although our strategy is application independent, the motivation came from an attempt to generate test scripts from MSC diagrams describing the behaviour of mobile phone devices.
References
[1]
Baker, P., Bristow, P., Jervis, C., King, D.J. and Mitchell, B., Automatic generation of conformance tests from message sequence charts. In: Sherratt, E. (Ed.), Lecture Notes in Computer Science, vol. 2599. pp. 170-198.
[2]
Booch, G., Rumbaugh, J. and Jacobson, I., The Unified Modeling Language User Guide. 1998. Addison Wesley, Reading, Massachusetts.
[3]
Broy, M., C. Hofmann, I. Kruger and M. Schmidt, Using extended event traces to describe communication in software architectures, in: Proceedings of the Asia-Pacific Software Engineering Conference and International Computer Science Conference (1997)
[4]
Buschmann, F., Meunier, R., Rohnert, H., Sommerlad, P. and Stal, M., Pattern-Oriented Software Architecture. Volume I: A System of Patterns. 1996. Wiley.
[5]
Cabral, G. and Sampaio, A., Formal specification generation from requirement documents. Electronic Notes in Theoretical Computer Science. v195. 171-188.
[6]
Damm, W. and Harel, D., LSCs: Breathing life into Message Sequence Charts. Formal Methods in System Design. v19. 45-80.
[7]
Engels, A.G., Mauw, S. and Reniers, M.A., A hierarchy of communication models for Message Sequence Charts. Science of Computer Programming. v44. 253-292.
[8]
“Failures-Divergence Refinement: FDR2 User Manual,” (2005)
[9]
Grosu, R., Kruger, I. and Stauner, T., Hybrid sequence charts. In: pp. 104
[10]
Isobe, Y. and Roggenbach, M., A generic theorem prover of CSP refinement. In: Halbwachs, N., Zuck, L.D. (Eds.), Lecture Notes in Computer Science, vol. 3440. pp. 108-123.
[11]
ITU-TS, ITU-TS recommendation Z.120: Message sequence chart 1999 (MSC99), Technical report, ITU-TS, Geneva (1999)
[12]
Ladkin, P.B. and Leue, S., What do Message Sequence Charts mean?. In: Proceedings of the IFIP TC6/WG6.1., pp. 301-316.
[13]
Mauw, S. and Reniers, M., A process algebra for Interworkings. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (Eds.), Handbook of Process Algebra, pp. 1269-1327.
[14]
Mauw, S. and Reniers, M.A., An algebraic semantics of basic Message Sequence Charts. The Computer Journal. v37. 269-278.
[15]
Melham, T.F., Abstraction mechanisms for hardware verification. In: Birtwistle, G., Subrahmanyam, P.A. (Eds.), VLSI Specification, Verification, and Synthesis, pp. 129-157.
[16]
Roscoe, A.W., Theory and Practice of Concurrency. 1998. Prentice-Hall.
[17]
Sengupta, B. and Cleaveland, R., Triggered Message Sequence Charts. IEEE Transactions on Software Engineering. v32. 587-607.
Recommendations
Adding time to synchronous process communications
Special Issue on Real-Time SystemsIn distributed real-time systems, communicating processes cannot be delayed for arbitrary amounts of time while waiting for messages. Thus, communication primitives used for real-time programming usually allow the inclusion of a deadline or timeout to ...
Bounded MSC communication
Message sequence charts (MSCs) and high-level message sequence charts (HMSCs) are popular formalisms for the specification of communication protocols between asynchronous processes. An important concept in this context is the size of the communication ...
Timing analysis of MSC specifications with asynchronous concatenation
Message Sequence Chart (MSC) is a graphical and textual language for describing the interactions between system components, and MSC specifications (MSSs) are a combination of a set of basic MSCs (bMSCs) and a High-level MSC that describes potentially ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Elsevier B.V. © 2009.
Publisher
Elsevier Science Publishers B. V.
Netherlands
Publication History
Published: 01 July 2009
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 25 Nov 2024
Other Metrics
Citations
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in