Algèbre de processus

Cet article est une ébauche concernant l’informatique.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

Pour les articles homonymes, voir Algèbre (homonymie).

Les algèbres de processus sont une famille de langages formels permettant de modéliser les systèmes (informatiques) concurrents ou distribués. Les algèbres de processus fournissent des outils formels permettant principalement de caractériser les interactions entre processus au sein d'un système concurrent ou distribué, les interactions prenant la forme d'échanges de messages. L'étude des algèbres de processus relève de l'informatique théorique, et leurs applications relèvent principalement du génie logiciel, en particulier des systèmes distribués.

Les différents calculs peuvent se distinguer par différents points : calcul synchrone ou asynchrone, calcul du premier ordre ou d'ordre supérieur (dans le second cas, les messages échangés sont des processus), etc.

Les principaux algèbres de processus utilisés sont :

• CSP (Communicating sequential processes) ;
• CCS ;
• LOTOS (Language Of Temporal Ordering Specification) - norme ISO 8807 ;
• Pi-calcul.

Histoire

La volonté de formaliser les systèmes concurrents se matérialise à la fin des années 1970 et au début des années 1980. Par exemple, Milner publie "A Calculus of Communicating Systems" en 1980^[1], qui présente CCS. Dans son introduction, Milner indique que le développement de CCS s'inscrit dans la lignée du développement des réseaux de Petri présenté en 1962 et de CSP (1978).

Principales constructions

Bien que les différentes algèbres comportent différentes constructions, des éléments de base (comme des primitives de communication ou de composition parallèle) se retrouvent au travers des différentes algèbres (avec parfois des différences subtiles).

Naturellement, les résultats et les caractéristiques de chaque algèbre dépendent des choix formels qui sont faits.

Le processus inactif

Les algèbres comprennent une notion de processus inactif ou terminé, qui caractérise un processus ne pouvant interagir avec le reste de l'environnement. Le plus souvent, ce processus est noté ${\displaystyle 0}$ ou ${\displaystyle NIL}$.

Composition séquentielle

La composition séquentielle permet de composer des actions ordonnées. Par exemple, dans CCS, la composition séquentielle est notée ${\displaystyle a.b.0}$, qui désigne un processus qui peut effectuer l'action ${\displaystyle a}$, puis l'action ${\displaystyle b}$.

Composition parallèle

La seconde forme de composition est la composition parallèle, qui indique des actions qui peuvent s'effectuer sans indication d'ordre. Toujours dans CCS, la composition parallèle est notée ${\displaystyle a|b}$, qui désigne un processus qui peut effectuer ${\displaystyle a}$ et ${\displaystyle b}$, dans n'importe quel ordre.

Communication

Bien que toutes les algèbres de processus intègrent une notion de communication entre processus, il y a une grande variabilité dans la manière dont les communications sont gérées.

Ainsi, par exemple, dans CCS, la communication consiste simplement en la synchronisation entre deux processus sur une action : si on a un processus ${\displaystyle a.0}$ et un processus ${\displaystyle {\overline {a}}.0}$ en parallèle, où ${\displaystyle {\overline {a}}}$ est l'action duale de ${\displaystyle a}$ (noté ${\displaystyle a.0\ |\ {\overline {a}}.0}$ comme vu dans la section précédente); alors les deux processus peuvent, atomiquement, effectuer l'action ${\displaystyle a}$ (resp. ${\displaystyle {\overline {a}}}$): ${\displaystyle a.0\ |\ {\overline {a}}.0}$ devient ${\displaystyle 0\ |\ 0}$.

Par ailleurs, il est possible d'avoir des formes plus complexes de communication. Par exemple, le ${\displaystyle \pi }$-calcul d'ordre supérieur permet l'échange de messages dont le contenu est lui-même un processus : ${\displaystyle a\langle P\rangle .0}$ désigne un processus qui envoie le processus ${\displaystyle P}$ sur le canal ${\displaystyle a}$; par ailleurs, un processus ${\displaystyle a(x).x}$ peut recevoir ce processus (lié à la variable ${\displaystyle x}$) et l'instancier : ${\displaystyle a\langle P\rangle .0\ |\ a(x).x}$ devient ${\displaystyle 0\ |\ P}$.

Enjeux de recherche

Cette section est vide, insuffisamment détaillée ou incomplète. Votre aide est la bienvenue pour synthétiser et rédiger quels sont les domaines de recherche actifs. !

• Portail de l’informatique