Special section on trends in verification and validationCompositional message sequence charts Elsa L. Gunter1, Anca Muscholl2 and Doron Peled3 | (1) | Department of Computer Science, New Jersey Institute of Technology, NJ 07102 Newark, USA |
| (2) | LIAFA, Université Paris 7, 2, place Jussieu, case 7014, 75251 Paris 05, France |
| (3) | Department of Electrical and Computer Engineering, The University of Texas at Austin, TX 78712 Austin, USA |
Published online: 18 December 2002 Abstract A message sequence chart (MSC) is a standard notation for describing the interaction between communicating objects. It is popular among the designers of communication protocols. MSCs enjoy both a visual and a textual representation. High-level MSCs (HMSCs) allow specifying infinite scenarios and different choices. Specifically, an HMSC consists of a graph, where each node is a finite MSC with matched send and receive events, and vice versa. In this paper we demonstrate a weakness of HMSCs, which disallows one to model certain interactions. We will show, by means of an example, that some simple finite state communication protocol cannot be represented using HMSCs. We then propose an extension to the MSC standard which allows HMSC nodes to include unmatched messages. The corresponding graph notation will be called HCMSC, which stands for high-level Compositional message sequence charts. With the extended framework, we provide an algorithm for automatically constructing an MSC representation for finite state asynchronous message passing protocols. Keywords Message sequence charts - Finite-state communication protocols - Partial-order methods
References
| 1. |
Alur, R., Etessami, K., Yannakakis, M.: Inference of message sequence charts. In: 22nd International Conference on Software Engineering, Limerick, Ireland. ACM, pp. 304–313, 2000 |
| |
| 2. |
Alur, R., Holzmann, G., Peled, D.: An analyzer for message sequence charts. In: Software Concepts Tools 17(2):70–77, 1996 |
| |
| 3. |
Alur, R., Peled, D., Penczek, W.: Model checking of causality properties. In: 10th Annual IEEE Symposium on Logic in Computer Science, LICS 95, San Diego, Calif., USA, pp. 90–100, 1995 |
| |
| 4. |
Alur, R., Yannakakis, Y.: Model checking of message sequence charts. In: Concurrency Theory, 10th International Conference, CONCUR99, Eindhoven, The Netherlands, Lecture Notes in Computer Science, vol. 1664. Springer, Berlin Heidelberg New York, 1999, pp. 114–129 |
| |
| 5. |
Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput Networks 14:25–59, 1987 |
| |
| 6. |
Esparza, E., Hansel, D, Rossmanith P, Schwoon S.: Efficient algorithms for model checking pushdown systems. In: Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, Ill., USA, Lecture Notes in Computer Science, vol. 1855. Springer, Berlin Heidelberg New York, 2000, pp. 232–247 |
| |
| 7. |
Godefroid, P.: Partial-order methods for the verification of concurrent systems – an approach to the state-explosion problem. Lecture Notes in Computer Science, vol. 1035. Springer, Berlin Heidelberg New York, 1996 |
| |
| 8. |
Godefroid, P., Wolper, P.: A partial approach to model checking. In: Inf Comput 110(2):305–326, 1994 |
| |
| 9. |
Gunter, E., Peled, D.: Path exploration tool. In: Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS 99, Amsterdam, The Netherlands, Lecture Notes in Computer Science, vol. 1579. Springer, Berlin Heidelberg New York, 1999, pp. 405–419 |
| |
| 10. |
Haugen, O.: Special issue of computer networks and ISDN systems on SDL and MSC, 1996 |
| |
| 11. |
Hélouët, L., Le Maigat, P.: Decomposition of message sequence charts. In: 2nd Workshop on SDL and MSC, SAM 2000, Grenoble, France, pp. 46–60, 2000 |
| |
| 12. |
Henriksen, J., Mukund, M., Narayan Kumar, K., Thiaga-
rajan, P.: On message sequence graphs and finitely generated regular MSC languages. In: Automata, Languages and Programming, 27th International Colloquium, ICALP 2000, Geneva, Switzerland, Lecture Notes in Computer Science, vol. 1853. Springer, Berlin Heidelberg New York, 2000,
pp. 675-686 |
| |
| 13. |
ITU-T Recommendation Z.120.: Message sequence chart (MSC), Geneva, 1996 |
| |
| 14. |
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Comm ACM 21:558–565, 1978 |
| |
| 15. |
Madhusudan, P.: Reasoning about sequential and branching behaviours of message sequence graphs. In: Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, Lecture Notes in Computer Science, vol. 2076. Springer, Berlin Heidelberg New York, 2001, pp. 809–820 |
| |
| 16. |
Mauw, S., Reniers, M.: High-level message sequence charts. In: SDL97: Time for Testing - SDL, MSC and Trends. Proc. SDL Forum97, 291–306, 1997 |
| |
| 17. |
Muscholl, A., Peled, D.: Message sequence graphs and decision problems on Mazurkiewicz traces. In: Mathematical Foundations of Computer Science 1999, 24th International Symposium, MFCS99, Szklarska Poreba, Poland, Lecture Notes in Computer Science, vol. 1999. Springer, Berlin Heidelberg New York, 1999, pp. 81–91 |
| |
| 18. |
Muscholl, A., Peled, D., Su, Z.: Deciding properties of message sequence charts. In: Foundations of Software Science and Computation Structure, 1st International Conference, FoSSaCS98, Lisbon, Portugal, Lecture Notes in Computer Science, vol. 1378. Springer, Berlin Heidelberg New York, 1998, pp. 226–242 |
| |
| 19. |
Muscholl, A., Peled, D.: High-level message sequence charts and finite-state communication protocols. In: Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, Lecture Notes in Computer Science, vol. 2076. Springer, Berlin Heidelberg New York, 2001, pp. 720–731 |
| |
| 20. |
Peled, D.: All from one, one for all: on model checking using representatives. In: Computer-Aided Verification, 5th International Conference, CAV 93, Elounda, Greece, Lecture Notes in Computer Science, vol. 697. Springer, Berlin Heidelberg New York, 1993, pp. 409–423 |
| |
| 21. |
Peled, D.: Specification and verification of message sequence charts. In: Formal Techniques for Distributed System Development, FORTE/PSTV 2000, Pisa, Italy. Kluwer, Boston, Mass., USA, pp. 139–154, 2000 |
| |
| 22. |
Tanenbaum, A.: Computer Networks. Prentice-Hall, Englewood Cliffs, N.J., USA, 1998 |
| |
|
|