Abstract
We discuss four issues concerning the semantics of Message Flow Graphs (MFGs). MFGs are extensively used as pictures of message-passing behavior. One type of MFG, Message Sequence Chart (MSC) is ITU Standard Z.120. We require that a system described by an MFG has global states with respect to its message-passing behavior, with transitions between these states effected by atomic message-passing actions. Under this assumption, we argue (a) that the collection of global message states defined by an MFG is finite (whether for synchronous, asynchronous, or partially-asynchronous message-passing); (b) that the unrestricted use of ‘conditions’ requires processes to keep control history variables of potentially unbounded size; (c) that allowing ‘crossing’ messages of the same type implies certain properties of the environment that are neither explicit nor desirable, and (d) that liveness properties of MFGs are more easily expressed by temporal logic formulas over the control states than by Büchi acceptance conditions over the same set of states.
This author’s work was partly supported by the Swiss National Science Foundation and the Swiss Federal Office for Education and Scientific Research.
Chapter PDF
Similar content being viewed by others
Keyword Codes
Keywords
References
B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Computing, 2: 117–126, 1987.
B. Alpern and F. B. Schneider. Verifying temporal properties without temporal logic. ACM Transactions on Programming Languages, 11 (1): 147–167, 1989.
F. Belina, D. Hogrefe, and A. Sarma. SDL with Applications from Protocol Specification. Prentice H ll International, 1991.
G. Berry and GL Gonthier. The Esterel synchronous programming language: design, semantics, implementation. Science of Computer Programming, 19: 87–152, 1992.
M. Broy. Towards a formal foundation of the specification and description language SDL. Formal Aspects of Computing, 3: 21–57, 1991.
CCITT. Recommendation Z.100: CCITT Specification and Description Language (SDL). CCITT, Geneva, 1992.
E. M. Clarke and R. P. Kurshan, editors. Computer Aided Verification: Proceedings of CAV’90, volume 531 of Lecture Notes in Computer Science. Springer Verlag, 1991.
C. Courcoubetis, editor. Computer Aided Verification: Proceedings of CAV’93, volume 697 of Lecture Notes in Computer Science. Springer Verlag, 1993.
J. De Man. Towards a formal semantics of message sequence charts. In [12], pages 157–166. 1993.
M. Diaz, J.-P. Ansart, J.-P. Courtiat, P. Azéma, and V. Chari, editors. The Formal Description Technique Estelle. North-Holland, 1989.
A.J.M. Donaldson. Specification of quality of service measurement points in JVTOS. Master’s thesis, University of Stirling, Scotland, U.K., September 1993.
O. Færgemand and A. Sarma, editors. SDL ‘83: Using Objects. North-Holland, 1993.
P. Graubmann, E. Rudolph, and J. Grabowski. Towards a Petri Net based semantics definition for Message Sequence Charts. In [12], pages 179–190. 1993.
C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21 (8): 666–677, August 1978.
G. J. Holzman. Design and Validation of Computer Protocols. Prentice-Hall International, 1991.
ITU. Recommendation Z.120: Message Sequence Chart (MSC). Geneva, 1993. Revised Version.
I. Jacobson. Object Oriented Software Engineering. 1992.
P. B. Ladkin and S. Leue. What do Message Sequence Charts mean? In [25]. 1994. To appear.
P.B. Ladkin and S. Leue. Interpreting message flow graphs. Formal Aspects of Computing, 1995. To appear.
P.B. Ladkin and B.B. Simons. Static Analysis of Interprocess Communication. Lecture Notes in Computer Science. Springer-Verlag, 1994. To appear.
K. G. Larsen and A. Skou, editors. Computer Aided Verification: Proceedings of CAV’91, volume 575 of Lecture Notes in Computer Science. Springer Verlag, 1992.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
S. Mauw, M. van Wijk, and T. Winter. A formal semantics of synchronous interworkings. In [12], pages 167–178. 1993.
J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, and W. Lorensen. Object-Oriented Modeling and Design. Prentice Hall International, 1991.
R. L. Tenney, P. D. Amer, and M. U. Uyar, editors. Formal Description Techniques, VI. IFIP Transactions C, Proceedings of the Sixth International Conference on Formal Description Techniques. North-Holland, 1994.
W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, chapter 4, pages 132–191. Elsevier Science Publishers B. V. ( North-Holland ), 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Ladkin, P.B., Leue, S. (1995). Four Issues Concerning the Semantics of Message Flow Graphs. In: Hogrefe, D., Leue, S. (eds) Formal Description Techniques VII. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34878-0_28
Download citation
DOI: https://doi.org/10.1007/978-0-387-34878-0_28
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2881-0
Online ISBN: 978-0-387-34878-0
eBook Packages: Springer Book Archive