Motivation et contexte du travail.

Des systèmes composés de programmes répartis sur plusieurs machines et liés les uns aux autres par une topologie de canaux complexe et changeante sont couramment utilisés dans le cadre d'applications de télécommunication à échelle industrielle. Par exemple, Ericsson a développé le langage Erlang qui permet de décrire de grands systèmes de processus communicants distribués au sein d'un réseau d'interconnexion changeant. Ce langage a été utilisé pour développer rapidement des services commerciaux complexes de téléphonie mobile qui auraient demandé un effort de conception considérable avec une programmation classique. Il est cependant très difficile de vérifier à priorien Erlang qu'un système composé de plusieurs milliers de processus et de canaux de communication ne comporte pas d'erreurs telles que : l'explosion du nombre de processus ou de canaux créés par le système (exhaustion des ressources), l'envoi d'informations par un processus sur un canal erroné (problèmes de confidentialité et de typage dynamique), le blocage d'un processus qui attend indéfiniment une information qui n'arrivera jamais (problèmes d'interblocages ou « deadlocks »). La difficulté vient du fait qu'il est nécessaire de connaître toute la dynamique de création des processus et des échanges de données pour détecter ces erreurs. Cette tâche est humainement infaisable pour de grands systèmes. Nous apportons une réponse possible à ces problèmes en utilisant les méthodes d'analyse statique de programmes par interprétation abstraite.

Sémantiques du pi-calcul.

Plutôt que de développer une analyse sur un langage particulier, nous utilisons le pi-calcul de R. Milner qui un modèle abstrait général qui concentre toutes les caractéristiques des systèmes de processus mobiles dans un formalisme simple. Il est à noter que le pi-calcul est à la base de la sémantique du langage Erlang. La sémantique classique du pi-calcul est fondée sur la réécriture de termes où la communication consiste en une substitution de noms tout comme en lambda-calcul. Le renommage implicite des noms de canaux par alpha-conversion et l'équivalence structurelle destinée à rapprocher les termes communicants rendent impossible l'identification précise des processus et des canaux créés lors de l'évolution du système. De ce fait la sémantique standard est inadéquate pour l'analyse statique du pi-calcul par interprétation abstraite. Une première étape a donc été de développer une hiérarchie de sémantiques non-standards du pi-calcul équivalentes à la sémantique standard traditionnelle, dans lesquelles les processus et les canaux créés sont identifiés de manière univoque par leur date de création dans l'histoire du système.

Analyse statique de la topologie des processus et communications (avec dénombrement).

Une première analyse statique du pi-calcul par interprétation abstraite a été développée qui permet de déterminer de façon précise des topologies de canaux non uniformes pour des systèmes de processus non bornés. L'abstraction repose sur une approximation des dates de création des processus et des canaux. Une date de création est donnée par une chaîne de symboles (correspondant à des points de contrôle dans le code décrivant le système de processus) tandis que la connectivité entre processus et canaux est représentée par un ensemble de relations binaires sur les dates de création. Le cúur de la représentation sémantique est donc donné par la notion de relation binaire sur un monoïde libre.

L'abstraction précise de telles relations binaires est très complexe. Les domaines des relations sont décrits par des automates réguliers. Le graphe des relations est abstrait par le graphe sur les vecteurs de Parikh sous-jacents. On utilise alors des treillis numériques abstraits pour représenter de façon finie des ensembles potentiellement infinis de vecteurs d'entiers. Cette représentation permet de décrire de façon fine des topologies de processus définis récursivement.

Cette analyse a été étendue pour obtenir des informations sur le nombre de processus et de canaux créés en modifiant la sémantique abstraite pour prendre en compte les instances de processus présents dans chaque configuration du système. Ces instances sont dénombrées en utilisant des treillis numériques abstraits afin de garantir la représentabilité d'une configuration abstraite. Les résultats fournis par cette analyse permettent de prouver automatiquement qu'un système de processus reste de taille bornée au cours de son évolution ou encore que certains processus ne sont jamais exécutés. De plus, la description très précise des communications entre les processus créés par le système est une aide précieuse pour le concepteur du système car elle donne un synoptique exhaustif des communications pouvant avoir lieu durant l'exécution du système.

Analyseurs prototypes.

Disponibles à l'adresse  http://di.ens.fr/~feret/.