La théorie du pi-calcul dans le système HOL - Université de Lorraine Accéder directement au contenu
Thèse Année : 1996

The pi-calculus theory in the HOL system

La théorie du pi-calcul dans le système HOL

Otmane Ait Mohamed
  • Fonction : Auteur
  • PersonId : 787553
  • IdRef : 128717025

Résumé

Not available
Le pi-calcul est un calcul de processus dont la théorie est assez proche de CCS d'une part et possédant une grande puissance d'expression d'autre part. On peut représenter une variété remarquable de notions qu'on retrouve dans les langages à haut niveau. Par exemple, le lambda-calcul, la transmission de processus et la localité de processus. On peut, également, coder d'une façon raisonnable les structures de données. De ce fait le pi-calcul est devenu l'exemple typique de calcul de processus mobile, ou la structure topologique entre les processus change dynamiquement au fur et à mesure que l'évolution du processus progresse. La mobilité dans ce calcul est dû au fait que les processus peuvent échanger des noms de canaux. L’objectif principal de la thèse est la réalisation d'un outil de preuve pour le pi-calcul. La simplicité de sa théorie basée sur un nombre restreint d’opérations et offrant des techniques de preuves basées sur la bisimulation permettent un traitement formel. Or, la plus grande partie des problèmes propres au pi-calcul porte sur des systèmes avec un nombre infini d'états sur lesquels les techniques de vérification automatiques échouent. C’est pourquoi, nous nous sommes orientés vers un système de preuve ouvert dans lequel on peut (1) formaliser les arguments mathématiques les plus sophistiques et (2) automatiser les parties répétitives d'une preuve. Notre choix s'est fait sur l'environnement de preuve HOL qui satisfait les deux conditions (1) et (2). En effet, HOL est basé sur une logique classique d'ordre supérieur et hérité du système LCF l'idée de tactics et tacticals ce qui permet une représentation directe et naturelle des arguments mathématiques et permet d'automatiser certaines parties de preuves. L’approche que nous avons adoptée pour représenter le pi-calcul dans HOL est une approche définitionnelle. C’est-à-dire nous avons présenté la syntaxe et la sémantique du pi-calcul dans la logique du système HOL. Dans ce cas les lois algébriques du pi-calcul sont dérivées formellement. Bien que cette approche soit difficile à mettre en œuvre, elle a l'avantage d'assurer la cohérence du système de preuve résultant. Dans l'environnement de preuve, pi-calcul-HOL, que nous baptisons PIC, on peut spécifier et prouver la correction des systèmes concurrents, soit par un raisonnement équationnel, soit par la technique de bisimulation. Cette approche nous permet de surmonter le problème de la vérification des systèmes à états infinis ou dont la structure est définie inductivement. Nous expérimentons le système sur la preuve de correction d'un protocole de communication, et sur l'étude du codage des entiers naturels dans le pi-calcul.
Fichier non déposé

Dates et versions

tel-01747761 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01747761 , version 1

Accès intranet

Citer

Otmane Ait Mohamed. La théorie du pi-calcul dans le système HOL. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1996. Français. ⟨NNT : 1996NAN10091⟩. ⟨tel-01747761⟩
49 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More