Comunicación de procesos secuenciales

La versión de CSP presentada en el artículo original de Hoare de 1978 era esencialmente un lenguaje de programación concurrente en lugar de un cálculo de procesos . Tenía una sintaxis sustancialmente diferente a la de versiones posteriores de CSP, no poseía una semántica definida matemáticamente ^{[ 12 ]} y era incapaz de representar el no determinismo ilimitado ^{[ 13 ]} . Los programas en el CSP original se escribían como una composición paralela de un número fijo de procesos secuenciales que se comunicaban entre sí estrictamente a través del paso de mensajes síncrono. A diferencia de versiones posteriores de CSP, a cada proceso se le asignaba un nombre explícito, y el origen o destino de un mensaje se definía especificando el nombre del proceso emisor o receptor previsto. Por ejemplo, el proceso

COPIA = *[c:carácter; oeste?c → este!c]

Recibe repetidamente un carácter del proceso llamado westy envía ese carácter al proceso llamado east. La composición paralela

[oeste::DESMONTAJE || X::COPIAR || este::MONTAJE]

asigna los nombres westal DISASSEMBLEproceso, Xal COPYproceso y eastal ASSEMBLEproceso, y ejecuta estos tres procesos simultáneamente. ^{[ 7 ]}

Tras la publicación de la versión original de CSP, Hoare, Stephen Brookes y AW Roscoe desarrollaron y perfeccionaron la teoría de CSP hasta su forma moderna de álgebra de procesos. El enfoque adoptado para desarrollar CSP como un álgebra de procesos estuvo influenciado por el trabajo de Robin Milner sobre el Cálculo de Sistemas de Comunicación (CCS) y viceversa. La versión teórica de CSP se presentó inicialmente en un artículo de 1984 de Brookes, Hoare y Roscoe, ^{[ 14 ]} y posteriormente en el libro de Hoare, Communicating Sequential Processes , ^{[ 12 ]} publicado en 1985. En septiembre de 2006, ese libro seguía siendo la tercera referencia de informática más citada de todos los tiempos según Citeseer (aunque una fuente poco fiable debido a la naturaleza de su muestreo). La teoría de CSP ha sufrido algunos cambios menores desde la publicación del libro de Hoare. La mayoría de estos cambios fueron motivados por la aparición de herramientas automatizadas para el análisis y la verificación de procesos CSP. El libro de Roscoe, The Theory and Practice of Concurrency ^{[ 1 ],} describe esta versión más reciente de CSP.

Una aplicación temprana e importante de CSP fue su uso para la especificación y verificación de elementos del Transputer INMOS T9000 , un procesador segmentado superescalar complejo diseñado para soportar el multiprocesamiento a gran escala . CSP se empleó para verificar la corrección tanto de la segmentación del procesador como del Procesador de Canal Virtual , que gestionaba las comunicaciones externas del procesador. ^{[ 9 ]}

La aplicación industrial de CSP al diseño de software se ha centrado generalmente en sistemas fiables y críticos para la seguridad. Por ejemplo, el Instituto de Sistemas Seguros de Bremen y Daimler-Benz Aerospace modelaron un sistema de gestión de fallos y una interfaz de aviónica (que consta de aproximadamente 23 000 líneas de código) destinados a su uso en la Estación Espacial Internacional en CSP, y analizaron el modelo para confirmar que su diseño estaba libre de interbloqueos y bloqueos permanentes . ^{[ 15 ] [ 16 ]} El proceso de modelado y análisis permitió descubrir una serie de errores que habrían sido difíciles de detectar solo mediante pruebas. De manera similar, Praxis High Integrity Systems aplicó el modelado y análisis de CSP durante el desarrollo de software (aproximadamente 100 000 líneas de código) para una autoridad de certificación de tarjetas inteligentes seguras para verificar que su diseño fuera seguro y estuviera libre de interbloqueos. Praxis afirma que el sistema tiene una tasa de defectos mucho menor que los sistemas comparables. ^{[ 10 ]}

Dado que CSP es idóneo para modelar y analizar sistemas que incorporan intercambios de mensajes complejos, también se ha aplicado a la verificación de protocolos de comunicación y seguridad. Un ejemplo destacado de este tipo de aplicación es el uso que hizo Lowe de CSP y del verificador de refinamiento FDR para descubrir un ataque previamente desconocido contra el protocolo de autenticación de clave pública Needham-Schroeder y, posteriormente, desarrollar un protocolo corregido capaz de contrarrestar dicho ataque. ^{[ 17 ]}

CSP proporciona dos clases de primitivas en su álgebra de procesos: eventos y procesos primitivos.

Eventos

Los eventos representan comunicaciones o interacciones. Se asume que son instantáneos, y su comunicación es todo lo que un "entorno" externo puede saber sobre los procesos. Un evento se comunica solo si el entorno lo permite. Si un proceso ofrece un evento y el entorno lo permite, entonces ese evento debe comunicarse. Los eventos pueden ser nombres atómicos (p. ej., encendido , apagado ), nombres compuestos (p. ej. , válvula.abrir , válvula.cerrar ) o eventos de entrada/salida (p. ej., ratón?xy , pantalla!mapa de bits ). El conjunto de todos los eventos se denota${\displaystyle \Sigma }$. ^{[ 18 ]}

Procesos primitivos

Los procesos primitivos representan comportamientos fundamentales: algunos ejemplos incluyen${\displaystyle \mathrm {STOP} }$(el proceso que se bloquea inmediatamente) y${\displaystyle \mathrm {SALTAR} }$(el proceso que finaliza inmediatamente con éxito). ^{[ 18 ]}

CSP tiene una amplia gama de operadores algebraicos. Los principales se presentan informalmente de la siguiente manera.

Prefijo

El operador de prefijo combina un evento y un proceso para producir un nuevo proceso. Por ejemplo,${\displaystyle a\to P}$es el proceso que está dispuesto a comunicar el evento${\displaystyle a}$con su entorno y, después${\displaystyle a}$se comporta como el proceso${\displaystyle P}$. ^{[ 18 ]}

Recursión

Los procesos se pueden definir mediante recursión. Donde${\displaystyle F(P)}$¿Es algún término de CSP que involucre?${\displaystyle P}$, el proceso${\displaystyle \mu PF(P)}$define un proceso recursivo dado por la ecuación ${\displaystyle P=F(P)}$. Las recursiones también pueden definirse mutuamente, como por ejemplo: $${\displaystyle {\begin{aligned}&P_{u}=arriba\to P_{d}\\&P_{d}=abajo\to P_{u}\\\end{aligned}}}$$ que define un par de procesos mutuamente recursivos que alternan entre comunicarse${\displaystyle arriba}$y${\displaystyle abajo}$. ^{[ 18 ]}

Elección determinista

El operador de elección determinista (o externo) permite definir la evolución futura de un proceso como una elección entre dos procesos componentes y permite que el entorno resuelva la elección comunicando un evento inicial para uno de los procesos. Por ejemplo,${\displaystyle (a\to P)\ \Box \ (b\to Q)}$es el proceso que está dispuesto a comunicar los eventos iniciales${\displaystyle a}$y${\displaystyle b}$y posteriormente se comporta como${\displaystyle P}$o${\displaystyle Q}$, dependiendo del evento inicial que el entorno elija comunicar. ^{[ 18 ]}

Elección no determinista

El operador de elección no determinista (o interno) permite definir la evolución futura de un proceso como una elección entre dos procesos componentes, pero no permite que el entorno tenga ningún control sobre cuál de los procesos componentes será seleccionado. Por ejemplo,${\displaystyle (a\to P)\sqcap (b\to Q)}$puede comportarse como cualquiera de las dos${\displaystyle a\to P}$o${\displaystyle b\to Q}$Puede negarse a aceptarlo.${\displaystyle a}$o${\displaystyle b}$y solo está obligado a comunicarse si el entorno ofrece ambas cosas.${\displaystyle a}$y${\displaystyle b}$.

El no determinismo puede introducirse inadvertidamente en una elección aparentemente determinista si los eventos iniciales de ambos lados de la elección son idénticos. Por ejemplo, $${\displaystyle (a\to a\to \mathrm {STOP} )\ \Box \ (a\to b\to \mathrm {STOP} )}$$y $${\displaystyle a\to {\big (}(a\to \mathrm {STOP} )\sqcap (b\to \mathrm {STOP} ){\big )}}$$ son equivalentes. ^{[ 18 ]}

Intercalación

El operador de intercalación representa una actividad concurrente completamente independiente. El proceso${\displaystyle P\;|||\;Q}$se comporta como ambos${\displaystyle P}$y${\displaystyle Q}$simultáneamente. Los eventos de ambos procesos se intercalan arbitrariamente en el tiempo. El intercalado puede introducir no determinismo incluso si${\displaystyle P}$y${\displaystyle Q}$ambos son deterministas: si${\displaystyle P}$y${\displaystyle Q}$ambos pueden comunicar el mismo evento, entonces${\displaystyle P\;|||\;Q}$elige de forma no determinista cuál de los dos procesos comunicó ese evento. ^{[ 18 ]}

Interfaz paralela

El operador de paralelismo de interfaz (o paralelismo generalizado) representa una actividad concurrente que requiere sincronización entre los procesos componentes: para${\displaystyle P\;|[X]|\;Q}$cualquier evento en el conjunto de interfaz${\displaystyle X\subseteq \Sigma }$solo puede ocurrir cuando ambos${\displaystyle P}$y${\displaystyle Q}$son capaces de participar en ese evento. ^{[ 18 ]}

Por ejemplo, el proceso${\displaystyle P\;|[\{a\}]|\;Q}$requiere que${\displaystyle P}$y${\displaystyle Q}$ambos deben poder realizar el evento${\displaystyle a}$antes de que ese evento pueda ocurrir. Entonces, el proceso${\displaystyle (a\to P)\;|[\{a\}]|\;(a\to Q)}$es equivalente a${\displaystyle a\to (P\;|[\{a\}]|\;Q)}$, mientras${\displaystyle (a\to P)\;|[\{a,b\}]|\;(b\to Q)}$es equivalente a${\displaystyle \mathrm {STOP} }$(es decir, el proceso se bloquea).

Ocultación

El operador de ocultación proporciona una forma de abstraer procesos haciendo que algunos eventos no sean observables por el entorno.${\displaystyle P\setminus X}$es el proceso${\displaystyle P}$con el evento programado${\displaystyle X}$oculto.

Un ejemplo trivial de ocultamiento es${\displaystyle (a\to P)\setminus \{a\}}$lo cual, suponiendo que el evento${\displaystyle a}$no aparece en${\displaystyle P}$, simplemente se reduce a${\displaystyle P}$Los eventos ocultos se internalizan como acciones τ , que son invisibles e incontrolables por el entorno. La existencia de ocultamiento introduce un comportamiento adicional llamado divergencia , donde se realiza una secuencia infinita de acciones τ. Esto es capturado por el proceso${\displaystyle \mathbf {div} }$, cuyo comportamiento consiste únicamente en realizar acciones τ para siempre. ^{[ 18 ]} Por ejemplo,${\displaystyle (\mu Pa\to P)\setminus \{a\}}$es equivalente a${\displaystyle \mathbf {div} }$.

Uno de los ejemplos arquetípicos de CSP es la representación abstracta de una máquina expendedora de chocolate y su interacción con una persona que desea comprar chocolate. Esta máquina expendedora puede realizar dos eventos diferentes: "moneda" y "chocolate", que representan la inserción del pago y la entrega del chocolate, respectivamente. Una máquina que exige el pago (solo en efectivo) antes de ofrecer un chocolate se puede escribir como:

$${\displaystyle \mathrm {Máquina expendedora} =\mathrm {moneda} \rightarrow \mathrm {choc} \rightarrow \mathrm {PARAR} }$$

Una persona que podría optar por usar una moneda o una tarjeta para realizar pagos podría modelarse de la siguiente manera:

$${\displaystyle \mathrm {Persona} =(\mathrm {moneda} \rightarrow \mathrm {STOP} )\;\Box \;(\mathrm {tarjeta} \rightarrow \mathrm {STOP} )}$$

Estos dos procesos pueden ponerse en paralelo, de modo que puedan interactuar entre sí. El comportamiento del proceso compuesto depende de los eventos en los que los dos procesos componentes deben sincronizarse. Por lo tanto,

$${\displaystyle \mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} ,\mathrm {card} \right\}\right]\right\vert \mathrm {Person} \equiv \mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} }$$

mientras que si la sincronización solo se requiriera en la “moneda”, obtendríamos

$${\displaystyle \mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} \right\}\right]\right\vert \mathrm {Person} \equiv \left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)}$$

Si abstraemos este último proceso compuesto ocultando los eventos de “moneda” y “carta”, es decir,

$${\displaystyle \left(\left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)\right)\setminus \left\{\mathrm {coin,card} \right\}}$$

obtenemos el proceso no determinista

$${\displaystyle \left(\mathrm {choc} \rightarrow \mathrm {STOP} \right)\sqcap \mathrm {STOP} }$$

Este es un proceso que ofrece un evento de "choque" y luego se detiene, o simplemente se detiene. En otras palabras, si consideramos la abstracción como una vista externa del sistema (por ejemplo, alguien que no ve la decisión tomada por la persona), se introduce el no determinismo .

La sintaxis de CSP define las formas “válidas” en que se pueden combinar procesos y eventos. Sea e un evento, b un valor booleano y X un conjunto de eventos. Entonces, la sintaxis básica de CSP se puede definir como:

$${\displaystyle {\begin{array}{lcll}{Proc}&::=&\mathrm {STOP} &\;\\&|&\mathrm {SKIP} &\;\\&|&e\rightarrow {Proc}&({\text{prefixing}})\\&|&{Proc}\;\Box \;{Proc}&({\text{external}}\;{\text{choice}})\\&|&{Proc}\;\sqcap \;{Proc}&({\text{nondeterministic}}\;{\text{choice}})\\&|&{Proc}\;\vert \vert \vert \;{Proc}&({\text{interleaving}})\\&|&{Proc}\;|[\{X\}]|\;{Proc}&({\text{interface}}\;{\text{parallel}})\\&|&{Proc}\setminus X&({\text{hiding}})\\&|&{Proc};{Proc}&({\text{sequential}}\;{\text{composition}})\\&|&\mathrm {if} \;b\;\mathrm {then} \;{Proc}\;\mathrm {else} \;Proc&({\text{boolean}}\;{\text{conditional}})\\&|&{Proc}\;\triangleright \;{Proc}&({\text{timeout}})\\&|&{Proc}\;\triangle \;{Proc}&({\text{interrupt}})\end{array}}}$$

Tenga en cuenta que, en aras de la brevedad, la sintaxis presentada anteriormente omite la${\displaystyle \mathbf {div} }$proceso, que representa la divergencia , así como varios operadores como el paralelismo alfabético, la canalización y las opciones indexadas.

CSP se ha dotado de varias semánticas formales diferentes , que definen el significado de las expresiones CSP sintácticamente correctas. La teoría de CSP incluye semántica denotacional mutuamente consistente , semántica algebraica y semántica operacional .

Los tres principales modelos denotacionales de CSP son el modelo de trazas , el modelo de fallos estables y el modelo de fallos/divergencias . Las asignaciones semánticas de expresiones de proceso a cada uno de estos tres modelos proporcionan la semántica denotacional para CSP. ^{[ 1 ]}

La semántica denotacional permite varias definiciones de un orden parcial de refinamiento en los procesos, que a su vez pueden usarse para representar elegantemente varias propiedades en los procesos. En general,${\displaystyle P\sqsubseteq Q}$denota${\displaystyle Q}$refina${\displaystyle P}$.

La herramienta CSP más conocida es probablemente Failures–Divergences Refinement (FDR), un producto comercial desarrollado originalmente por Formal Systems (Europe) Ltd. FDR se describe a menudo como un verificador de modelos , pero técnicamente es un verificador de refinamiento , ya que convierte dos expresiones de proceso CSP en sistemas de transición etiquetados (LTS) y luego determina si uno de los procesos es un refinamiento del otro dentro de algún modelo semántico especificado (trazas, fallos o fallos/divergencia). ^{[ 20 ]} FDR aplica varios algoritmos de compresión del espacio de estados a los LTS de proceso para reducir el tamaño del espacio de estados que debe explorarse durante una verificación de refinamiento. FDR fue sucedido por FDR2, FDR3 y FDR4. ^{[ 21 ]}

El Adelaide Refinement Checker ( ARC ) ^{[ 22 ]} es un verificador de refinamiento CSP desarrollado por el Formal Modelling and Verification Group de la Universidad de Adelaida . ARC se diferencia de FDR2 en que representa internamente los procesos CSP como diagramas de decisión binarios ordenados (OBDD), lo que alivia el problema de la explosión de estados de las representaciones LTS explícitas sin requerir el uso de algoritmos de compresión de espacio de estados como los utilizados en FDR2.

El proyecto ProB , ^{[ 23 ]} alojado en el Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, se creó originalmente para apoyar el análisis de especificaciones construidas con el método B. Sin embargo, también incluye soporte para el análisis de procesos CSP mediante verificación de refinamiento y verificación de modelos LTL . ProB también puede utilizarse para verificar propiedades de especificaciones combinadas de CSP y B. FDR3 integra un animador ProBE CSP.

El Process Analysis Toolkit (PAT) ^{[ 24 ] [ 25 ]} es una herramienta de análisis CSP desarrollada en la Escuela de Computación de la Universidad Nacional de Singapur . PAT puede realizar comprobación de refinamiento, comprobación de modelos LTL y simulación de procesos CSP y Timed CSP. El lenguaje de procesos PAT extiende CSP con soporte para variables compartidas mutables, paso de mensajes asíncrono y una variedad de construcciones de procesos relacionadas con el tiempo y la equidad cuantitativa como deadliney waituntil. El principio de diseño subyacente del lenguaje de procesos PAT es combinar un lenguaje de especificación de alto nivel con programas procedimentales (por ejemplo, un evento en PAT puede ser un programa secuencial o incluso una llamada a una biblioteca C# externa) para una mayor expresividad. Las variables compartidas mutables y los canales asíncronos proporcionan un azúcar sintáctico conveniente para patrones de modelado de procesos bien conocidos utilizados en CSP estándar. La sintaxis de PAT es similar, pero no idéntica, a CSP _M . ^{[ 26 ]} Las principales diferencias entre la sintaxis PAT y el estándar CSP _M son el uso de punto y coma para terminar las expresiones de proceso, la inclusión de azúcar sintáctico para variables y asignaciones, y el uso de una sintaxis ligeramente diferente para la elección interna y la composición paralela.

VisualNets ^{[ 27 ]} produce visualizaciones animadas de sistemas CSP a partir de especificaciones y admite CSP temporizado.

CSPsim ^{[ 28 ]} es un simulador perezoso. No realiza una verificación de modelo de CSP, pero es útil para explorar sistemas muy grandes (potencialmente infinitos).

SyncStitch ^{[ 29 ]} es un verificador de refinamiento CSP con un entorno interactivo de modelado y análisis. Cuenta con un editor gráfico de diagramas de transición de estados. El usuario puede modelar el comportamiento de los procesos no solo como expresiones CSP, sino también como diagramas de transición de estados. Los resultados de la verificación se presentan gráficamente como árboles de cálculo y pueden analizarse de forma interactiva con herramientas de inspección periféricas. Además de las verificaciones de refinamiento, puede realizar verificaciones de interbloqueo y de bloqueo permanente.