Note publique d'information : La these étudie les protocoles de communication asynchrones. Elle se compose de deux
parties. Dans la première on décrit brièvement des formalismes existants qui sont
à la base de beaucoup de modèles de communication asynchrone et on introduit formellement
les notions de speed-independence et delay-insensitivity. Un protocole est speed-independent
s'il garantit la correction indépendamment de la vitesse de computation de chaque
module. Un protocole est delay-insensitive s'il est speed-independent et il garantit
la correction indépendamment des retards de propagation dans les communications. La
deuxième partie contient la plupart des contributions originelles. Le but est de fournir
un étude formel du protocole handshake, un protocole delay-insensitive qui fait alterner
les deux partenaires dans chaque communication. D'abord on rappelle [vb:93], le seul
modèle formel précédent du protocole handshake. Ensuite on montre un défaut de ce
modèle, qui ne représente pas correctement la composition de systèmes.Dans notre analyse
on introduit un modèle à jeux, un avec les réseaux de petri et un calcul de processus.
Le modèle à jeux est un modèle à traces comme [vb:93]. La composition y est définie
correctement mais certains comportements handshake ne sont pas représentés. Le modèle
à réseaux de petri, qui est correct et complet par rapport à tous les comportements
handshake, résolue ce problème. Enfin on propose un calcul de processus à la ccs,
qui fournit une syntaxe correcte au protocole handshake. On montre aussi que l'interprétation
du calcul dans les réseaux est fully abstract et telle que tout réseau fini est l'interprétation
d'une configuration dans le calcul.
Note publique d'information : The thesis deals with communication protocols in an asynchronous environment. It can
be divided in two parts. In the first part we briefly survey existing formalisms and
tools which underlie many models of asynchronous communication and we formally introduce
the notions of speed-independence and delay-insensitivity. A protocol is speed-independent
if it ensures correctness independently of the computational speeds of single modules.
A protocol is delay-insensitive if it is speed-independent and ensures correctness
independently of propagation delays in communications. The second part contains most
of the original contributions. It aims at providing a formal study of the handshake
protocol, a delay-insensitive protocol which requires that the two partners invouved
in a communication alternats. We start by recalling [vb:93], the only previous formal
model of the handshake protocol. We also identify a limitation of that model, as we
show that its representation of the composition of systems is not correct. In our
analysis we introduce a game semantics model, a petri nets model and a process calculus.
The game semantics model is a trace model as [vb:93], it defines composition correctly
but fails to represent some handshake behaviors. The petri nets model instead, is
correct and complete with respecj to all handshake behaviors. The process calculus
is in ccs style. We show its correctness as a syntax for the handshake protocol and
we provide an interpretation from the calculus to the petri nets model, which is fully
abstract and such that any finite net is the interpretation of some configuration
in the calculus.
paprika.idref.fr
data.idref.fr
Documentation
