🧮 CSP — Communicating Sequential Processes
Algèbre de processus créée par Sir Tony Hoare (1978) · Fondements formels de la concurrence · FDR4, ProB, PAT · Influence sur Go, Erlang, Clojure
1934–2026 · Oxford · Microsoft Research Cambridge
🍗 In Memoriam — Sir Charles Antony Richard Hoare
"There are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies. The first method is far more difficult."
— Tony Hoare, Turing Award Lecture, 1980
— Tony Hoare, Turing Award Lecture, 1980
Sir Tony Hoare est décédé le 5 mars 2026, à l'âge de 92 ans. Diplômé de Merton College (Classiques & Philosophie, Oxford), il découvrit Quicksort en 1959 à Moscou, développa le premier compilateur ALGOL 60 commercial chez Elliott Brothers, puis devint Professeur à Queen's University Belfast (1968) avant de rejoindre Oxford (1977) où il dirigea le Programming Research Group jusqu'en 2000.
Il rejoignit ensuite Microsoft Research Cambridge comme chercheur principal, poursuivant ses travaux sur la sémantique unifiée de la programmation concurrente. Élu Fellow de la Royal Society en 1982, il fut anobli en 2000, lauréat du Turing Award 1980, du Kyoto Prize 2000, de la médaille John von Neumann IEEE (2011) et de la Royal Medal (2023).
Ses contributions fondatrices : Quicksort (1959), Hoare Logic (1969), le concept de moniteur pour la synchronisation (1974), CSP (1978), et l'aveu célèbre sur la null reference — sa « billion-dollar mistake ».
📐 CSP : définition & modèles sémantiques
CSP (Communicating Sequential Processes) est un langage formel de description des interactions entre processus concurrents, membre de la famille des algèbres de processus. Introduit par Tony Hoare en 1978 (article ACM), reformulé théoriquement avec Stephen Brookes et A.W. Roscoe en 1984–1985. Le modèle est fondé sur la communication synchrone par rendez-vous (canaux sans mémoire intermédiaire).
CSP propose trois modèles sémantiques emboîtés, du plus abstrait au plus complet :
Modèle des Traces
traces(P) ⊆ Σ*
Un processus est caractérisé par l'ensemble des séquences d'événements observables qu'il peut produire. Modèle le plus simple : ignore les refus et la divergence. Suffit pour vérifier la sûreté des séquences d'interactions.
Modèle Stable Failures
(traces, refusals)
Extension du modèle des traces : chaque trace est associée aux ensembles d'événements refusables dans les états stables. Permet de vérifier le déterminisme et de détecter les interblocages (deadlocks) potentiels.
Modèle Failures/Divergences
(failures, divergences)
Modèle complet enrichi des traces de divergence — séquences menant à une boucle interne infinie. Permet la vérification de la vivacité (livelock-freedom) et la sémantique complète du raffinement CSP.
Relation de raffinement :
Q ⊑ P signifie que Q raffine P — tout comportement de Q est admis par P. C'est le fondement des vérificateurs comme FDR4 : on vérifie qu'une implémentation raffine sa spécification.
⚙️ Opérateurs algébriques
| Opérateur | Notation | Description |
|---|---|---|
| STOP | STOP | Processus en interblocage immédiat (deadlock). N'accepte aucun événement. |
| SKIP | SKIP | Terminaison réussie. Communique le signal interne ✓ puis s'arrête. |
| Préfixage | a → P | Communiquer l'événement a, puis se comporter comme P. Brique fondamentale. |
| Choix externe | P ☐ Q | L'environnement choisit entre P et Q selon le premier événement offert. Déterministe. |
| Choix interne | P ⊓ Q | Le processus choisit non-déterministement entre P et Q, sans signal à l'environnement. |
| Entrelacement | P ||| Q | P et Q s'exécutent de façon totalement indépendante et entrelacée, sans synchronisation. |
| Parallèle d'interface | P |[X]| Q | P et Q se synchronisent sur les événements de l'ensemble X, s'entrelacent sur les autres. |
| Parallèle total | P || Q | P et Q se synchronisent sur tous les événements communs (|[α P ∩ α Q]|). |
| Masquage (Hiding) | P \ X | Rend les événements de X internes (invisibles à l'observateur). Permet l'abstraction. |
| Renommage | P[[a/b]] | Renomme l'événement b en a dans le comportement de P. Utilisé pour le câblage de composants. |
| Composition séquentielle | P ; Q | Exécute P jusqu'à SKIP, puis enchaîne avec Q. Modélise la séquence dans les systèmes terminants. |
| Interruption | P △ Q | P peut être interrompu par Q à tout moment. Modélise les exceptions et les préemptions. |
| Récursion | μ P . F(P) | Point fixe — définit les processus réactifs infinis. Base des systèmes non-terminants. |
| Réplication | ||| i : S • P(i) | Entrelacement indexé sur un ensemble S. Crée des collections paramétriques de processus. |
🔧 Outils formels
FDR4 CommercialGratuit acad.
Failures-Divergences Refinement · Oxford / Cocotec · v4.2.7
Vérificateur de raffinement de référence. Prend en entrée du CSPM (CSP + langage fonctionnel). Vérifie le raffinement dans les trois modèles sémantiques, détecte deadlocks et livelocks, supporte les systèmes jusqu'à plusieurs milliards d'états via parallélisation multi-cœurs et clustering. Inclut Probe (animateur interactif) et un visualiseur de contre-exemples.
ProB Open source
Heinrich-Heine-Universität Düsseldorf
Animateur et model-checker pour la méthode B, Event-B et CSP. Supporte l'analyse CSP || B (intégration CSP + méthode B) et la vérification LTL. Interface ProB 2.0 basée sur Eclipse. Exportation vers nuSMV et d'autres model-checkers. Activement maintenu.
PAT Gratuit
Process Analysis Toolkit · NUS Singapore
Vérificateur de raffinement, model-checker LTL et simulator pour CSP, CSP temporisé et d'autres algèbres de processus. Supporte les variables partagées et la communication asynchrone. Interface graphique Windows. Utilisé dans l'enseignement universitaire en Asie.
SyncStitch
IPA Japan · Nagoya University
Environnement de modélisation et vérification CSP avec éditeur graphique de processus. Analyse de deadlock, vérification de raffinement. Développé dans le cadre du projet IPA Exploratory Software au Japon.
Circus / CML Académique
University of York / York & Copenhagen
Circus intègre CSP et Z (notation de spécification par prédicats). CML (Circus Modelling Language) étend Circus pour les systèmes cyber-physiques collaboratifs. Cible les systèmes critiques avec état explicite et comportement concurrent.
Timed CSP / TCSP
Extension temps-réel
Extension de CSP avec contraintes temporelles quantitatives. Permettre de spécifier des délais, des timeouts, des échéances. Fondement théorique des vérificateurs pour systèmes embarqués temps-réel. Supporte les urgences et les délais optionnels.
🌐 Influence sur les langages modernes
Go (Golang)
Google · Rob Pike & Ken Thompson · 2009
Go est la réalisation la plus directe des idées CSP dans un langage industriel. Les goroutines sont des processus CSP légers (M:N threading), les channels sont les canaux de communication synchrone (ou bufferisée). La devise : "Don't communicate by sharing memory; share memory by communicating." Rob Pike cite explicitement CSP comme inspiration fondamentale de Go.
Erlang / Elixir
Ericsson · Joe Armstrong · 1986
Erlang est né pour les systèmes téléphoniques Ericsson. Son modèle d'acteurs — processus légers isolés + passage de messages — est directement inspiré de CSP, bien qu'il préfère les mailboxes asynchrones aux canaux synchrones. OTP (Open Telecom Platform) = framework CSP industriel de fait. Elixir hérite de ce modèle via la BEAM.
Clojure core.async
Rich Hickey · 2013
La bibliothèque
core.async de Clojure implémente CSP explicitement : channels bufferisés ou non, go blocks (coroutines légères), alts! (choix externe CSP). Rich Hickey a publié une conférence détaillant pourquoi CSP est supérieur aux callbacks et aux futures pour la composition de systèmes asynchrones.Crystal / occam
occam · INMOS · Transputer · 1983
occam est le premier langage de programmation directement basé sur CSP, conçu pour programmer les processeurs Transputer INMOS. Parallélisme par
PAR, synchronisation par ALT (choix gardé de Dijkstra). Influence directe sur les processeurs parallèles embarqués des années 1980–90. occam-π étend occam avec les π-calcul (mobilité de canaux).Haskell STM & IORef
Simon Peyton Jones · GHC
Haskell propose deux approches complémentaires à CSP : Software Transactional Memory (STM) pour la mémoire partagée transactionnelle, et les MVars/Channels (
Control.Concurrent.Chan) pour le passage de messages à la CSP. La bibliothèque Control.Concurrent.CML implémente le Concurrent ML (variant CSP fonctionnel).Kotlin coroutines / Swift actors
JetBrains · Apple · 2021+
Les Kotlin Flows et Channels dans le framework coroutines reprennent les sémantiques CSP (rendezvous, fan-out, fan-in). Les Swift Actors (Swift 5.5, 2021) introduisent l'isolation par acteur inspirée du modèle CSP/Erlang pour garantir la sûreté en concurrence sans locks.
🏭 Applications industrielles & académiques
Vérification de processeurs
INMOS T9000 Transputer · 1994–1995
Vérification formelle complète du pipeline interne du processeur T9000 d'INMOS à l'aide de CSP et FDR. Premier exemple industriel majeur de vérification formelle d'un processeur commercial. A permis de découvrir plusieurs bugs de timing avant fabrication.
Systèmes avioniques ISS
Bremen Institute for Safe Systems · ~1999
Spécification et vérification CSP d'un système avionique de la Station Spatiale Internationale. 23 000 lignes de spécification CSP. Démonstration de la scalabilité de l'approche formelle sur des systèmes embarqués critiques de grande taille.
Sécurité des smart-cards
Praxis High Integrity Systems
Spécification et vérification de l'autorité de certification pour smart-cards : 100 000 lignes de code formel. Utilisation de CSP pour modéliser les protocoles cryptographiques et garantir la correction des interfaces de sécurité.
Protocoles de sécurité
Gavin Lowe · Oxford · 1995
Gavin Lowe utilisa CSP et FDR pour découvrir une attaque sur le protocole Needham-Schroeder (1978), qui avait été considéré sûr pendant 17 ans. Cette découverte révolutionna l'analyse formelle des protocoles cryptographiques et mena directement au protocole NSL corrigé.
Systèmes ferroviaires
Siemens / Thales / RATP
CSP et ses variants (Timed CSP, Circus) sont utilisés pour la spécification des systèmes de signalisation et de contrôle-commande ferroviaires (norme EN 50128 SIL4). Vérification des interlockings, gestion des cantons, protocoles de sécurité ETCS.
Recherche académique 2023–2026
Oxford · York · Southampton · NUS
Travaux récents : CSP pour les systèmes cyber-physiques (CML/Circus), intégration CSP + model learning (inférer des modèles CSP par observation), CSP probabiliste (vérification quantitative), et applications aux protocoles de smart contracts blockchain.
📰 Actualités & Ressources
Événements récents
05 mars 2026
Décès de Sir Tony Hoare — In Memoriam (Oxford)
Sir Charles Antony Richard Hoare s'est éteint à l'âge de 92 ans. Turing Award 1980, père de CSP, QuickSort, Hoare Logic et du concept de moniteur. Oxford University a publié un mémorial sur son site.
2023
ProB 2.0 — Nouvelles fonctionnalités de vérification CSP
L'équipe HHU Düsseldorf continue d'améliorer ProB 2.0 avec de meilleures performances pour l'analyse CSP || B et le support de nouveaux dialectes d'Event-B.
2023–2024
Circus / CML — Systèmes cyber-physiques
L'Université de York poursuit le développement de Circus pour les systèmes collaboratifs cyber-physiques (CPS), en partenariat avec des industriels du secteur aérospatial et ferroviaire.
Continu
Go — Évolutions du modèle de concurrence CSP
Le langage Go continue d'enrichir son modèle CSP : améliorations du scheduler, nouvelles primitives dans
sync et context, sémantiques renforcées pour les channels avec generics (Go 1.21+).Ressources fondamentales
Livre fondateur — Hoare 1985
Communicating Sequential Processes · Prentice-Hall
L'ouvrage de référence de Tony Hoare. Disponible gratuitement en ligne depuis 2004. Décrit les fondements mathématiques complets de CSP, de la syntaxe aux modèles sémantiques.
The Theory and Practice of Concurrency
A.W. Roscoe · Oxford · 1997 (révisé 2010)
Le livre de référence moderne sur CSP par Bill Roscoe. Couvre les trois modèles sémantiques, FDR, les patterns d'utilisation et les applications industrielles. Accessible en ligne.
Article original — Hoare 1978
CACM Vol. 21, No. 8 · ACM Digital Library
L'article fondateur de 1978 "Communicating Sequential Processes" publié dans Communications of the ACM. Introduit pour la première fois le modèle de communication par canal et les opérateurs essentiels.
Hoare Logic (1969)
An Axiomatic Basis for Computer Programming · CACM
Parallèlement à CSP, Hoare développa la logique qui porte son nom : les triplets de Hoare
{P} S {Q}. Fondement de la vérification de programmes impératifs, précurseur de la logique de séparation (O'Hearn, Reynolds, Yang — 2001).Turing Award Lecture 1980
The Emperor's Old Clothes · CACM
Discours de réception du Turing Award par Hoare. Plaidoyer pour la simplicité dans la conception logicielle et critique des langages trop complexes. Contient la citation célèbre sur les deux façons de concevoir un logiciel.
Wikipedia CSP (EN)
Références académiques complètes
Article Wikipedia anglophone très complet sur CSP : historique, opérateurs, modèles sémantiques, outils, langages influencés et bibliographie complète.