Modélisation formelle d’une architecture logicielle pour la  simulation numérique

Le π-calcul

Le π-calcul est une algèbre de processus au même titre que CSP [Hoa86] ou CCS [Mil89]. Ces algèbres proposent des méthodes formelles afin de modéliser des interactions entre processus. Les modélisations réalisées permettent de construire un modèle mathématique afin de garantir la cohérence du modèle et la conformité du programme. Dans le π-calcul, un terme bien formé dénote un processus et les processus se synchronisent et échangent des noms.

Notons que le πcalcul ne fait aucune hypothèse sur les vitesses d’exécution relatives des différents processus, qui sont donc présumés progresser chacun à leur rythme. Dans cette section, nous détaillons différentes versions du π-calcul. Nous commençons par une introduction en présentant sa forme la plus simple, le π-calcul monadique (Section 2.1.1), nous continuons par sa forme polyadique (Section 2.1.1.5).

Enfin, nous terminons par le π-calcul d’ordre supérieur (Section 2.1.2) qui nous permet de modéliser des agents mobiles (cf. Section 1.4). 2.1.1 Introduction au π-calcul Nous commençons cette section par quelques définitions et conventions concernant le π-calcul monadique du premier ordre. Nous finissons par un exemple simple pour introduire la notion de mobilité offerte par le π-calcul. 

Conventions de nommage

Nous considérons une ensemble infini de noms N, notés a, b, . . . , z, qui représentent des canaux de communications, des données et des variables, et un ensemble de termes (nous les nommons également processus ou agent), noté typiquement P , Q , R . . ., qui représentent des processus. A partir du tableau 2.1, nous pouvons noter qu’un agent π-calcul peut prendre les formes suivantes : – α.P dénote la préfixation d’un processus P par une action α. Le préfixe α peut prendre les formes suivantes : – a(x) dénote le réception de la valeur, stockée dans la variable x, via le canal a.

Ce préfixe lie le nom x au processus P. – a h x i dénote l’émission de la valeur, stockée dans la variable x, via le canal a. Ce préfixe ne lie pas le nom x au processus P. – τ dénote une action interne, non observable. – P   Q met en parallèle deux processus P et Q. Les processus P et Q peuvent agir indépendamment l’un de l’autre mais peuvent aussi agir l’un sur l’autre. – P + Q permet le choix entre le processus P et le processus Q. – ! P peut être considéré comme une composition infinie P   P   · · ·   P. – [x = y] P définit que le processus évolue comme P si x et y sont identiques. 

Congruence structurelle

Une congruence est une relation intéressante à définir pour les équivalences comportementales. Cette propriété permet par exemple de décomposer les processus étudiés en sous-termes, de prouver l’équivalence sur cette décomposition et d’en déduire l’équivalence des termes initiaux par congruence.

 Sémantique opérationnelle

Une sémantique opérationnelle est très utile pour calculer l’évolution d’un terme. La sémantique opérationnelle de π-calcul est donnée par un système de transitions étiquetées, où les transitions sont du type P α −−−→ P ′ avec α un ensemble d’actions pouvant être l’action interne τ , l’action de réception a(x) et l’action d’émission a h x i.

Cette relation de réduction signifie que P est transformé en P ′ suite à l’action α. La transition a(x).P a(u) −−−−→ P{u/x} signifie que si le nom u est transmis à travers le canal a alors le processus a(x).P qui attend un nom sur le canal a reçoit le nom u et effectue une substitution 3 de x par u et se comporte ensuite comme P, où toutes les occurrences de x sont remplacées par u