Sujet : Synthesis for distributed asynchronous systems

Responsable : Igor Walukiewicz
Téléphone : 69 17
e-mail : voir la page web
Site Web : http://www.labri.fr/Perso/~igw/
Equipe : LAAA

Présentation du sujet :

One of the most difficult parts of a system design is the design and
control of communication patterns between components. One way to avoid
this difficulty would be to synthesize a correct system from a given
specification. For synthesis to work one needs: (i) a way to model
systems, (ii) a specification language, and (iii) the algorithms for
generating systems from specifications. All three are not
immediate. As for models, one can considered communicating automata or
statecharts. For specifications one can have program logics or message
sequence chart based formalisms. The later, while less studied, are
better adapted to express properties of communication
patterns. Finally, one needs the algorithms, and several are already
presented in the literature.

The objective of this thesis is development of synthesis methods based
on communication pattern requirements. The main difference from better
studied cases of synthesis is that here we assume that the
communication is done via unbounded buffers and not through a
rendez-vous mechanism. The change to unbounded buffers modifies the
problem substantially, in particular the properties one wants to
verify are often not regular. The goal of this thesis would be to
develop a language for describing communication patterns and the
synthesis algorithms for this language.

Mot-clés : Message Sequent Charts, synthesis

Références :
(All the papers are available from the author's pages.)

D. Harel and H. Kugler, "Synthesizing State-Based Object Systems from
LSC Specifications", Int. J. of Foundations of Computer Science 13:1
(2002), 5-51.

A. Stefanescu, J. Esparza, A. Muscholl. Synthesis of Distributed
Algorithms Using Asynchronous Automata , Proc. of CONCUR'03, Lecture
Notes in Computer Science 2761, pp. 27--41, 2003.

Synthesizing distributed finite-state systems from MSCs M. Mukund,
K. Narayan Kumar and M. Sohoni Proc. CONCUR '00, Springer LNCS 1877
(2000) 521-535.