Formal Methods for Message Sequence Charts

Doron Peled
Bell Laboratories, USA

Abstract

The ISO standard for MSC provides a useful tool for 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.