Calcul des systèmes communicants - Calculus of communicating systems

Le calcul des systèmes communicants ( CCS ) est un calcul de processus introduit par Robin Milner vers 1980 et le titre d'un livre décrivant le calcul. Ses actions modélisent des communications indivisibles entre exactement deux participants. Le langage formel comprend des primitives pour décrire la composition parallèle, le choix entre les actions et la restriction de portée. CCS est utile pour évaluer l'exactitude qualitative des propriétés d'un système telles que l' interblocage ou le livelock .

Selon Milner, "Il n'y a rien de canonique dans le choix des combinateurs de base, même s'ils ont été choisis avec une grande attention à l'économie. Ce qui caractérise notre calcul n'est pas le choix exact des combinateurs, mais plutôt le choix de l'interprétation et du cadre mathématique ".

Les expressions de la langue sont interprétées comme un système de transition étiqueté . Entre ces modèles, la bissimilarité est utilisée comme équivalence sémantique.

Syntaxe

Etant donné un ensemble de noms d'actions, l'ensemble des processus CCS est défini par la grammaire BNF suivante :

${\displaystyle P::=0\,\,\,|\,\,\,a.P_{1}\,\,\,|\,\,\,A\,\,\,|\, \,\,P_{1}+P_{2}\,\,\,|\,\,\,P_{1}|P_{2}\,\,\,|\,\,\,P_{ 1}[b/a]\,\,\,|\,\,\,P_{1}{\ backslash }a\,\,\,}$

Les parties de la syntaxe sont, dans l'ordre donné ci-dessus

processus inactif

le processus inactif est un processus CCS valide${\style d'affichage 0}$

action

le processus peut effectuer une action et continuer comme le processus${\displaystyle a.P_{1}}$${\style d'affichage a}$${\style d'affichage P_{1}}$

identifiant de processus

écrire pour utiliser l'identifiant pour faire référence au processus (qui peut contenir l'identifiant lui-même, c'est-à-dire que les définitions récursives sont autorisées)${\displaystyle A{\overset {\underset {\mathrm {def} }{}}{=}}P_{1}}$${\style d'affichage A}$${\style d'affichage P_{1}}$${\style d'affichage A}$

choix

le processus peut se dérouler en tant que processus ou processus${\style d'affichage P_{1}+P_{2}}$${\style d'affichage P_{1}}$${\style d'affichage P_{2}}$

composition parallèle

${\style d'affichage P_{1}|P_{2}}$raconte que les processus et existent simultanément${\style d'affichage P_{1}}$${\style d'affichage P_{2}}$

renommer

${\displaystyle P_{1}[b/a]}$est le processus avec toutes les actions nommées renommées en${\style d'affichage P_{1}}$${\style d'affichage a}$${\style d'affichage b}$

restriction

${\displaystyle P_{1}{\backslash }a}$est le processus sans action${\style d'affichage P_{1}}$${\style d'affichage a}$

Calculs, modèles et langages associés

• Les processus séquentiels communicants (CSP), développés par Tony Hoare , sont un langage formel apparu à la même époque que le CCS.
• L' algèbre des processus communicants (ACP) a été développée par Jan Bergstra et Jan Willem Klop en 1982, et utilise une approche axiomatique (dans le style de l'algèbre universelle ) pour raisonner sur une classe de processus similaire à celle du CCS.
• Le pi-calcul , développé par Robin Milner , Joachim Parrow et David Walker à la fin des années 80, étend le CCS à la mobilité des liens de communication, en permettant aux processus de communiquer eux-mêmes les noms des canaux de communication.
• PEPA , développé par Jane Hillston, introduit la synchronisation des activités en termes de taux distribués de manière exponentielle et de choix probabiliste, permettant d'évaluer les mesures de performance.
• Les Systèmes Concurrents Communicants Réversibles (RCCS) introduits par Vincent Danos , Jean Krivine et d'autres, introduisent la réversibilité (partielle) dans l'exécution des processus CCS.

Quelques autres langages basés sur CCS :

• Calcul des systèmes de diffusion
• Langue de spécification de commande temporelle (LOTOS)
• Process Calculus for Spatially-Explicit Ecological Models (PALPS) est une extension de CCS avec un choix probabiliste, des emplacements et des attributs pour les emplacements
• Moteur d'interprétation du langage Java Orchestration (Jolie)

Modèles qui ont été utilisés dans l'étude des systèmes de type CCS :

• Monoïde historique
• Modèle d'acteur

Les références

• Robin Milner : Un calcul des systèmes de communication , Springer Verlag, ISBN  0-387-10235-3 . 1980.
• Robin Milner, Communication and Concurrency , Prentice Hall, International Series in Computer Science, ISBN  0-13-115007-3 . 1989