Specification and verification using Message Sequence Charts
LIAFA, case 7014
2 place Jussieu
75251 Paris Cedex 05, France
In this talk we present an overview of recent results on the use of Message
Sequence Charts (MSC) as a graphical specification formalism for communicating
distributed processes. We consider several questions concerning the expressivity
of the model and algorithmic verification of properties.
We first present the class of finite-state high-level MSCs, that exhibits
tight connections with Mazurkiewicz traces, . For this class, Mukund et
al. and very recently Kuske  showed the equivalence between definability
second-order logic and acceptance by message passing automata.
In the second part we consider infinite-state high-level MSCs and the realizability
by message passing automata. We present subclasses of infinite-state high-level
MSCs that can be realized by such automata with or without deadlocks. These
results extend recent work of Alur et al.  and have been presented
at ICALP'02, .
 R. Alur, K. Etessami, and M. Yannakakis. Realizability and verification
of MSC graphs. In: ICALP 2001
, LNCS 2076
, pp. 797-808,
 B. Genest, A. Muscholl, H. Seidl and M. Zeitoun. Infinite-state High-Level
MSCs: Model-Checking and Realizability. In: ICALP 2002
, LNCS 2380
, pp. 657-668, Springer 2002.
 D. Kuske. A further step towards a theory of regular MSC languages. In:
, LNCS 2285
, pp. 489-500, Springer 2002.
 M. Mukund, K. Narayan Kumar and M. Sohoni. Synthesizing distributed finite-state
systems from MSCs. In: CONCUR 2000
, LNCS 1877
, pp. 521-535,