Formal Methods for Message Sequence Charts

The ISO standard for MSC provides a useful tool fro visualizing communication protocols. MSCs present a model for concurrency that is different from the model of finite state systems, used frequently in automated verification. Thus, the MSC model poses new and interesting problems related to automatic verification of communication protocols. In this paper, some of the recent results related to MSCs are surveyed.