Communication des processus séquentiels

La version de CSP présentée dans l'article original de Hoare de 1978 était essentiellement un langage de programmation concurrent plutôt qu'un calcul de processus . Sa syntaxe différait sensiblement des versions ultérieures de CSP, elle ne possédait pas de sémantique mathématiquement définie et était incapable de représenter le non-déterminisme illimité . Les programmes en CSP original étaient écrits comme une composition parallèle d'un nombre fixe de processus séquentiels communiquant entre eux strictement par échange de messages synchrone. Contrairement aux versions ultérieures de CSP, chaque processus se voyait attribuer un nom explicite, et la source ou la destination d'un message était définie en spécifiant le nom du processus émetteur ou récepteur. Par exemple, le processus

COPIE = *[c:caractère; ouest?c → est!c]

reçoit de manière répétée un caractère du processus nommé westet envoie ce caractère au processus nommé east. La composition parallèle

[ouest::DÉSASSEMBLE || X::COPIE || est::ASSEMBLE]

attribue les noms westau DISASSEMBLEprocessus, Xau COPYprocessus et eastau ASSEMBLEprocessus, et exécute ces trois processus simultanément.

Suite à la publication de la version originale de CSP, Hoare, Stephen Brookes et A.W. Roscoe ont développé et affiné la théorie de CSP pour lui donner sa forme moderne d'algèbre de processus. L'approche adoptée pour développer CSP en une algèbre de processus a été influencée par les travaux de Robin Milner sur le calcul des systèmes communicants (CCS), et réciproquement. La version théorique de CSP a été initialement présentée dans un article de 1984 par Brookes, Hoare et Roscoe , puis dans l'ouvrage de Hoare, *Communicating Sequential Processes * , publié en 1985. En septembre 2006, ce livre figurait encore parmi les ouvrages de référence en informatique les plus cités de tous les temps, selon Citeseer (bien que cette source soit sujette à caution en raison de la nature de son échantillonnage). La théorie de CSP a subi quelques modifications mineures depuis la publication de l'ouvrage de Hoare. La plupart de ces modifications ont été motivées par l'avènement d'outils automatisés pour l'analyse et la vérification des processus CSP. L' ouvrage de Roscoe, *The Theory and Practice of Concurrency , décrit cette nouvelle version de CSP.

Une des premières applications importantes du CSP a été son utilisation pour la spécification et la vérification des éléments du transputer INMOS T9000, un processeur superscalaire pipeliné complexe conçu pour prendre en charge le multiprocesseur à grande échelle . Le CSP a été employé pour vérifier la correction du pipeline du processeur et du processeur de canal virtuel , qui gérait les communications hors puce pour le processeur.

L'application industrielle de la programmation par contraintes (CSP) à la conception logicielle s'est généralement concentrée sur les systèmes fiables et critiques pour la sécurité. Par exemple, l'Institut de Brême pour les systèmes sûrs et Daimler-Benz Aerospace ont modélisé un système de gestion des pannes et une interface avionique (environ 23 000 lignes de code) destinés à la Station spatiale internationale à l'aide de la CSP, puis ont analysé le modèle pour confirmer l'absence de blocages et d'interblocages . Le processus de modélisation et d'analyse a permis de mettre au jour plusieurs erreurs difficiles à détecter par des tests seuls. De même, Praxis High Integrity Systems a appliqué la modélisation et l'analyse CSP lors du développement d'un logiciel (environ 100 000 lignes de code) pour une autorité de certification de cartes à puce sécurisées, afin de vérifier la sécurité et l'absence de blocages de sa conception. Praxis affirme que le système présente un taux de défauts bien inférieur à celui des systèmes comparables.

Le CSP étant particulièrement adapté à la modélisation et à l'analyse de systèmes intégrant des échanges de messages complexes, il a également été appliqué à la vérification des protocoles de communication et de sécurité. Un exemple notable de ce type d'application est l'utilisation par Lowe du CSP et du vérificateur de raffinement FDR pour découvrir une attaque jusque-là inconnue contre le protocole d'authentification à clé publique de Needham-Schroeder , puis pour développer un protocole corrigé capable de contrer cette attaque.

CSP fournit deux classes de primitives dans son algèbre de processus : les événements et les processus primitifs.

Événements

Les événements représentent des communications ou des interactions. Ils sont considérés comme instantanés, et leur communication est la seule information qu'un environnement externe puisse avoir sur les processus. Un événement n'est communiqué que si l'environnement le permet. Si un processus génère un événement et que l'environnement le permet, alors cet événement doit être communiqué. Les événements peuvent être désignés par des noms atomiques (par exemple, activé , des noms composés (par exemple, ) ou des événements d'entrée/sortie (par exemple, ). L'ensemble de tous les événements est noté .

Processus primitifs

Les processus primitifs représentent des comportements fondamentaux : par exemple,

CSP dispose d'une vaste gamme d'opérateurs algébriques. Les principaux sont présentés de manière informelle comme suit.

Préfixe

L'opérateur de préfixe combine un événement et un processus pour produire un nouveau processus. Par exemple,

Récursivité

Les processus peuvent être définis à l'aide de la récursivité. Où

Choix déterministe

L'opérateur de choix déterministe (ou externe) permet de définir l'évolution future d'un processus comme un choix entre deux processus composants et permet à l'environnement de résoudre ce choix en communiquant un événement initial pour l'un des processus. Par exemple,

Choix non déterministe

L'opérateur de choix non déterministe (ou interne) permet de définir l'évolution future d'un processus comme un choix entre deux processus composants, mais ne permet pas à l'environnement de contrôler lequel des processus composants sera sélectionné. Par exemple,

Le non-déterminisme peut s'introduire involontairement dans un choix apparemment déterministe si les événements initiaux des deux parties sont identiques. Ainsi, par exemple,

entrelacement

L'opérateur d'entrelacement représente une activité concurrente totalement indépendante. Le processus

Interface parallèle

L'opérateur parallèle d'interface (ou parallèle généralisé) représente une activité concurrente qui nécessite une synchronisation entre les processus composants : pour

Par exemple, le processus

Dissimulation

L'opérateur de masquage permet d'abstraire les processus en rendant certains événements inobservables par l'environnement.

Un exemple trivial de dissimulation estd'actions τ , invisibles et incontrôlables par l'environnement. L'existence de cette dissimulation introduit un comportement supplémentaire appelé divergence , où une séquence infinie d'actions τ est exécutée. Ce phénomène est capturé par le processus

Un exemple archétypal de CSP est la représentation abstraite d'un distributeur automatique de chocolat et de ses interactions avec une personne souhaitant en acheter. Ce distributeur peut effectuer deux événements distincts, « pièce » et « chocolat », représentant respectivement l'insertion d'un moyen de paiement et la distribution d'un chocolat. Un distributeur exigeant un paiement (uniquement en espèces) avant de délivrer un chocolat peut être décrit comme suit :

On pourrait modéliser une personne susceptible de choisir d'utiliser une pièce ou une carte pour effectuer des paiements comme suit :

Ces deux processus peuvent être mis en parallèle afin d'interagir. Le comportement du processus composite dépend des événements sur lesquels les deux processus composants doivent se synchroniser. Ainsi,

alors que si la synchronisation n'était requise que sur la « pièce », nous obtiendrions

Si nous faisons abstraction de ce dernier processus composite en masquant les événements « pièce » et « carte », c’est-à-dire,

nous obtenons le processus non déterministe

Il s'agit d'un processus qui, soit propose un événement « choc » puis s'arrête, soit s'arrête tout simplement. Autrement dit, si l'on considère l'abstraction comme une vision externe du système (par exemple, celle d'une personne qui ignore la décision prise par l'individu), on introduit le non-déterminisme .

La syntaxe de CSP définit les manières « légales » de combiner des processus et des événements. Soit un booléen et

Notez que, par souci de concision, la syntaxe présentée ci-dessus omet le

Le CSP est doté de plusieurs sémantiques formelles qui définissent la signification des expressions syntaxiquement correctes. La théorie du CSP comprend une sémantique dénotationnelle , une sémantique algébrique et une sémantique opérationnelle mutuellement cohérentes .

Les trois principaux modèles dénotationnels du CSP sont le modèle des traces , le modèle des défaillances stables et le modèle des défaillances/divergences . Les correspondances sémantiques entre les expressions de processus et chacun de ces trois modèles fournissent la sémantique dénotationnelle du CSP.

La sémantique dénotationnelle permet plusieurs définitions d'un ordre de raffinement partiel sur les processus, qui peuvent à leur tour être utilisées pour représenter élégamment plusieurs propriétés des processus. Généralement,raffine

L'outil CSP le plus connu est probablement Failures–Divergences Refinement (FDR), un produit commercial initialement développé par Formal Systems (Europe) Ltd. Souvent décrit comme un vérificateur de modèles , FDR est en réalité un vérificateur de raffinements . Il convertit deux expressions de processus CSP en systèmes de transition étiquetés (LTS), puis détermine si l'un des processus raffine l'autre au sein d'un modèle sémantique spécifié (traces, défaillances ou défaillances/divergence). FDR applique divers algorithmes de compression d'espace d'états aux LTS des processus afin de réduire la taille de l'espace d'états à explorer lors d'une vérification de raffinement. FDR a été remplacé par FDR2, FDR3 et FDR4.

L' outil de vérification de raffinement d'Adélaïde ( ARC ) est un vérificateur de raffinement CSP développé par le groupe de modélisation et de vérification formelles de l'Université d'Adélaïde . ARC diffère de FDR2 en ce qu'il représente en interne les processus CSP sous forme de diagrammes de décision binaires ordonnés (OBDD), ce qui atténue le problème d'explosion d'états des représentations LTS explicites sans nécessiter l'utilisation d'algorithmes de compression d'espace d'états tels que ceux utilisés dans FDR2.

Le projet ProB , hébergé par l'Institut für Informatik de l'Université Heinrich-Heine de Düsseldorf, a été initialement conçu pour faciliter l'analyse des spécifications construites selon la méthode B. Il prend également en charge l'analyse des processus CSP, notamment par la vérification du raffinement et la vérification de modèles LTL . ProB permet aussi de vérifier les propriétés des spécifications combinant CSP et B. Un module d'animation CSP ProBE est intégré à FDR3.

Le Process Analysis Toolkit (PAT) est un outil d'analyse CSP développé à la Faculté d'informatique de l' Université nationale de Singapour . PAT permet d'effectuer des vérifications de raffinement, des vérifications de modèles LTL et des simulations de processus CSP et CSP temporisés. Le langage de processus PAT étend CSP en prenant en charge les variables partagées mutables, la transmission asynchrone de messages et diverses constructions de processus équitables et quantitatives liées au temps, telles que ` deadlinefor` et `for` waituntil. Le principe de conception sous-jacent du langage de processus PAT est de combiner un langage de spécification de haut niveau avec des programmes procéduraux (par exemple, un événement dans PAT peut être un programme séquentiel ou même un appel à une bibliothèque C# externe) pour une plus grande expressivité. Les variables partagées mutables et les canaux asynchrones offrent une syntaxe simplifiée pour les modèles de processus bien connus utilisés dans CSP standard. La syntaxe PAT est similaire, mais non identique, à celle de CSP _M. Les principales différences entre la syntaxe PAT et la norme CSP _M sont l'utilisation de points-virgules pour terminer les expressions de processus, l'inclusion de sucre syntaxique pour les variables et les affectations, et l'utilisation d'une syntaxe légèrement différente pour le choix interne et la composition parallèle.

VisualNets produit des visualisations animées de systèmes CSP à partir de spécifications et prend en charge le CSP temporisé.

CSPsim est un simulateur paresseux. Il ne vérifie pas le modèle CSP, mais est utile pour explorer des systèmes très grands (potentiellement infinis).

SyncStitch est un outil de vérification du raffinement des CSP doté d'un environnement interactif de modélisation et d'analyse. Il intègre un éditeur graphique de diagrammes de transition d'état. L'utilisateur peut modéliser le comportement des processus non seulement sous forme d'expressions CSP, mais aussi de diagrammes de transition d'état. Les résultats de la vérification sont également présentés graphiquement sous forme d'arbres de calcul et peuvent être analysés interactivement à l'aide d'outils d'inspection périphériques. Outre les vérifications de raffinement, il permet d'effectuer des vérifications d'interblocage et de blocage actif.