Modeling the Handshake protocal for Asychrony
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
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.
Abstract FR:
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.