Le concept de réversibilité est ancien, mais il soulève de nos jours beaucoup d'intérêt. Il est en effet exploité dans de nombreux domaines tels que la conception de circuits, le débogage et le test de programmes, la simulation et l'informatique quantique. L'idée d'un modèle de programmation réversible peut se montrer particulièrement intéressante pour la construction de systèmes sûrs de fonctionnement, ne serait-ce que parce que plusieurs techniques connues pour la construction de tels systèmes exploitent une forme ou une autre de retour en arrière ou de reprise. Nous poursuivons dans cette thèse l'étude entreprise avec CCS réversible par Vincent Danos et Jean Krivine, en définissant un pi-calcul d'ordre supérieur réversible (rhopi). Nous prouvons que le modèle obtenu est causalement cohérent, et que l'on peut encoder fidèlement rhopi dans une variante du pi-calcul d'ordre supérieur. Nous définissons également une primitive de reprise à grain fin qui permet de contrôler le retour en arrière dans une exécution concurrente. Nous spécifions formellement la sémantique de cette primitive, et nous montrons qu'elle possède de bonnes propriétés, y compris en présence d'opérations de reprise concurrentes. Enfin nous définissons un algorithme concurrent implantant cette primitive de reprise et ous montrons que cet algorithme respecte la sémantique définie.

Le modèle des Acteurs, introduit par HEWITT et AGHA à la fin des années 80, décrit un système concurrent comme un ensemble d'agents autonomes au comportement non uniforme et communiquant de façon point-à-point par l'envoi de messages étiquetés. Le calcul CAP, proposé par COLAÇO, est un calcul de processus basé sur ce modèle qui permet de décrire sans encodage complexe des systèmes réalistes non triviaux. Ce calcul permet, entre autre, la communication de comportements via les messages et est, en ce sens, un calcul d'ordre supérieur. L'analyse de propriétés sur ce calcul a déjà fait l'objet de plusieurs travaux, essentiellement par inférence de type en utilisant des types comportementaux et du sous-typage.<br /> Par ailleurs, des travaux plus récents, effectués par VENET puis FERET, proposent une utilisation de l'interprétation abstraite pour l'analyse de calculs de processus. Ces approches permettent de calculer des propriétés non uniformes : elles permettent, par exemple, de différencier les instances récursives d'un même processus.<br /> Cette thèse s'inscrit donc dans la suite de ces deux approches, en appliquant l'interprétation abstraite à l'analyse de CAP. Suivant le cadre proposé par FERET, CAP est, tout d'abord, exprimé dans une forme non standard facilitant les analyses. L'ensemble des configurations atteignables est ensuite sur-approximé via une représentation, correcte par construction, dans des domaines abstraits.<br /> Des domaines abstraits généraux sont ensuite introduits afin d'améliorer les analyses existantes ou de représenter des propriétés locales à un sous-terme.<br /> Des propriétés spécifiques à CAP, la linéarité des termes et l'absence de messages orphelins, sont alors étudiées dans ce cadre. Des domaines spécifiques sont définis et utilisés pour vérifier ces propriétés. Le cadre présenté permet de lever toutes les restrictions existantes des analyses précédentes quant à la forme des termes ou l'utilisation du passage de comportement.<br /> L'intégralité des analyses présentées a été implantée dans un prototype.

Le concept de réversibilité est ancien, mais il soulève de nos jours beaucoup d'intérêt. Il est en effet exploité dans de nombreux domaines tels que la conception de circuits, le débogage et le test de programmes, la simulation et l'informatique quantique. L'idée d'un modèle de programmation réversible peut se montrer particulièrement intéressante pour la construction de systèmes sûrs de fonctionnement, ne serait-ce que parce que plusieurs techniques connues pour la construction de tels systèmes exploitent une forme ou une autre de retour en arrière ou de reprise. Nous poursuivons dans cette thèse l'étude entreprise avec CCS réversible par Vincent Danos et Jean Krivine, en définissant un pi-calcul d'ordre supérieur réversible (rhopi). Nous prouvons que le modèle obtenu est causalement cohérent, et que l'on peut encoder fidèlement rhopi dans une variante du pi-calcul d'ordre supérieur. Nous définissons également une primitive de reprise à grain fin qui permet de contrôler le retour en arrière dans une exécution concurrente. Nous spécifions formellement la sémantique de cette primitive, et nous montrons qu'elle possède de bonnes propriétés, y compris en présence d'opérations de reprise concurrentes. Enfin nous définissons un algorithme concurrent implantant cette primitive de reprise et ous montrons que cet algorithme respecte la sémantique définie. / Reversible computing has a long history. Nowadays, reversible computing is attracting increasing interest because of its potential applications in diverse fields, including hardware design, biological modelling, program debugging and testing and quantum computing. Of particular interest is the application of reversible computation notions to the study of programming abstractions for dependable systems, because several techniques used to build dependable systems rely on some forms of undo or rollback. We continue, in this thesis, the study undertaken on reversible CCS by Vincent Danos and Jean Krivine, by defining a reversible higher-order pi-calculus (rhopi). We prove that reversibility in our calculus is causally consistent and that one can encode faithfully rhopi into a variant of HOpi. Moreover we design a fine-grained rollback primitive able to control the rollback of a concurrent execution. We give a formal specification of this primitive and show that it enjoys good properties, even in presence of concurrent conflicting rollbacks. We then devise a concurrent algorithm implementing such primitive and show that the algorithm respects the defined semantics.