Specification and verification using Message Sequence Charts
Anca Muscholl
LIAFA, case 7014
Université Paris-7
2 place Jussieu
75251 Paris Cedex 05, France
anca.muscholl@liafa.jussieu.fr
http://www.liafa.jussieu.fr/~anca/
Abstract
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, [1]. For this class, Mukund et
al.[4] and very recently Kuske [1] showed the equivalence between definability
in monadic
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. [1] and have been presented
at ICALP'02, [2].
References
[1] R. Alur, K. Etessami, and M. Yannakakis. Realizability and verification
of MSC graphs. In:
ICALP 2001, LNCS
2076, pp. 797-808,
Springer 2001.
[2] 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.
[3] D. Kuske. A further step towards a theory of regular MSC languages. In:
STACS 2002, LNCS
2285, pp. 489-500, Springer 2002.
[4] M. Mukund, K. Narayan Kumar and M. Sohoni. Synthesizing distributed finite-state
systems from MSCs. In:
CONCUR 2000, LNCS
1877, pp. 521-535,
Springer 2000.