En informática , la comunicación de procesos secuenciales ( CSP ) es un lenguaje formal para describir patrones de interacción en sistemas concurrentes . [1] Es un miembro de la familia de teorías matemáticas de concurrencia conocidas como álgebras de procesos, o cálculos de procesos , basadas en el paso de mensajes a través de canales . CSP fue muy influyente en el diseño del lenguaje de programación occam [1] [2] y también influyó en el diseño de lenguajes de programación como Limbo , [3] RaftLib , Go , [4] Crystal y core.async de Clojure . [5]
La CSP fue descrita por primera vez en un artículo de 1978 por Tony Hoare , [6] pero desde entonces ha evolucionado sustancialmente. [7] La CSP se ha aplicado prácticamente en la industria como una herramienta para especificar y verificar los aspectos concurrentes de una variedad de sistemas diferentes, como el T9000 Transputer , [8] así como un sistema de comercio electrónico seguro. [9] La teoría de la CSP en sí también es todavía objeto de investigación activa, incluido el trabajo para aumentar su rango de aplicabilidad práctica (por ejemplo, aumentar la escala de los sistemas que se pueden analizar de manera manejable). [10]
Historia
La versión de CSP presentada en el artículo original de 1978 de Hoare 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 las versiones posteriores de CSP, no poseía una semántica definida matemáticamente [11] y era incapaz de representar el no determinismo ilimitado . [12] Los programas en el CSP original se escribieron como una composición paralela de un número fijo de procesos secuenciales que se comunican entre sí estrictamente a través del paso de mensajes sincrónico. A diferencia de las versiones posteriores de CSP, a cada proceso se le asignó un nombre explícito y el origen o destino de un mensaje se definió especificando el nombre del proceso de envío o recepción previsto. Por ejemplo, el proceso
COPY = * [c: carácter; oeste? c → este! c]
recibe repetidamente un carácter del proceso named west
y envía ese carácter al proceso named east
. La composición paralela
[oeste :: DESMONTAJE || X :: COPIA || este :: MONTAJE]
asigna los nombres west
al DISASSEMBLE
proceso, X
al COPY
proceso y east
al ASSEMBLE
proceso, y ejecuta estos tres procesos al mismo tiempo. [6]
Tras la publicación de la versión original de CSP, Hoare, Stephen Brookes y AW Roscoe desarrollaron y refinaron la teoría de CSP en su forma algebraica de proceso moderna. El enfoque adoptado para desarrollar CSP en un álgebra de procesos fue 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, [13] y más tarde en el libro de Hoare Communicating Sequential Processes , [11] que se publicó en 1985. En septiembre de 2006, ese libro seguía siendo el tercera referencia de ciencias de la computación más citada de todos los tiempos según Citeseer [ cita requerida ] (aunque una fuente poco confiable debido a la naturaleza de su muestreo). La teoría de la CSP ha sufrido algunos cambios menores desde la publicación del libro de Hoare. La mayoría de estos cambios fueron motivados por la llegada de herramientas automatizadas para el análisis y la verificación de procesos de CSP. The Theory and Practice of Concurrency [1] de Roscoe describe esta nueva versión de CSP.
Aplicaciones
Una aplicación temprana e importante de CSP fue su uso para la especificación y verificación de los elementos de la INMOS T9000 Transputer , un complejo de procesador segmentado superescalar diseñado para soportar multiprocesamiento a gran escala. Se empleó CSP para verificar la corrección tanto de la canalización del procesador como del Procesador de canal virtual, que administraba las comunicaciones fuera del chip para el procesador. [8]
La aplicación industrial de CSP al diseño de software generalmente se ha centrado en sistemas confiables 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 fallas y una interfaz de aviónica (que consta de aproximadamente 23.000 líneas de código) para su uso en la Estación Espacial Internacional en CSP, y analizaron el modelo para confirmar que su diseño estaba libre de interbloqueo y bloqueo activo. [14] [15] El proceso de modelado y análisis fue capaz de descubrir una serie de errores que habrían sido difíciles de detectar utilizando únicamente las pruebas. Del mismo modo, Praxis High Integrity Systems aplicó el modelado y análisis de CSP durante el desarrollo del software (aproximadamente 100.000 líneas de código) para que una autoridad de certificación de tarjetas inteligentes segura verificara que su diseño era seguro y no estaba bloqueado. Praxis afirma que el sistema tiene una tasa de defectos mucho menor que los sistemas comparables. [9]
Dado que CSP se adapta bien al modelado y análisis de sistemas que incorporan intercambios de mensajes complejos, también se ha aplicado a la verificación de protocolos de seguridad y comunicaciones. Un ejemplo destacado de este tipo de aplicación es el uso de CSP y el verificador de refinamiento FDR de Lowe's para descubrir un ataque previamente desconocido en el protocolo de autenticación de clave pública Needham-Schroeder y luego desarrollar un protocolo corregido capaz de derrotar el ataque. [dieciséis]
Descripción informal
Como sugiere su nombre, CSP permite la descripción de sistemas en términos de procesos componentes que operan de forma independiente e interactúan entre sí únicamente a través de la comunicación de paso de mensajes. Sin embargo, la parte "secuencial" del nombre de CSP es ahora un nombre inapropiado, ya que la CSP moderna permite que los procesos de componentes se definan como procesos secuenciales y como la composición paralela de procesos más primitivos. Las relaciones entre los diferentes procesos y la forma en que cada proceso se comunica con su entorno se describen utilizando varios operadores algebraicos de procesos . Usando este enfoque algebraico, se pueden construir fácilmente descripciones de procesos bastante complejas a partir de unos pocos elementos primitivos.
Primitivos
CSP proporciona dos clases de primitivas en su álgebra de procesos:
- Eventos
- Los eventos representan comunicaciones o interacciones. Se supone que son indivisibles e instantáneos. Pueden ser nombres atómicos (por ejemplo en , fuera ), los nombres compuestos (por ejemplo valve.open , valve.close ), o de entrada / salida (por ejemplo, eventos de ratón? Xy , pantalla! Mapa de bits ).
- Procesos primitivos
- Los procesos primitivos representan comportamientos fundamentales: los ejemplos incluyen STOP (el proceso que no comunica nada, también llamado interbloqueo ) y SKIP (que representa una terminación exitosa).
Operadores algebraicos
CSP tiene una amplia gama de operadores algebraicos. Los principales son:
- Prefijo
- El operador de prefijo combina un evento y un proceso para producir un nuevo proceso. Por ejemplo,
- es el proceso que está dispuesto para comunicarse una con su entorno y, después de una , se comporta como el proceso P .
- Elección determinista
- El operador de elección determinista (o externo) permite que la evolución futura de un proceso se defina 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,
- es el proceso que está dispuesto para comunicar los eventos iniciales un y b y posteriormente se comporta como sea P o Q , dependiendo de qué evento inicial los elige de entorno para comunicarse. Si tanto una y b se comunicaron al mismo tiempo, la elección se resolvería nondeterministically.
- 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 al entorno ningún control sobre cuál de los procesos componentes se seleccionará. Por ejemplo,
- puede comportarse como o . Puede negarse a aceptar a o b y solo está obligado a comunicarse si el entorno ofrece tanto a como b . El no determinismo puede introducirse inadvertidamente en una elección nominalmente determinista si los eventos iniciales de ambos lados de la elección son idénticos. Así por ejemplo,
- es equivalente a
- Entrelazado
- El operador de entrelazado representa una actividad concurrente completamente independiente. El proceso
- se comporta como P y Q simultáneamente. Los eventos de ambos procesos se intercalan arbitrariamente en el tiempo.
- Interfaz paralela
- El operador paralelo de interfaz representa una actividad concurrente que requiere sincronización entre los procesos componentes: cualquier evento en el conjunto de interfaces solo puede ocurrir cuando todos los procesos componentes pueden participar en ese evento. Por ejemplo, el proceso
- requiere que P y Q sean capaces de realizar el evento a antes de que ese evento pueda ocurrir. Entonces, por ejemplo, el proceso
- puede participar en el evento ay convertirse en el proceso
- tiempo
- simplemente se interbloqueará.
- Ocultación
- El operador de ocultación proporciona una forma de abstraer procesos al hacer que algunos eventos no sean observables. Un ejemplo trivial de esconderse es
- que, asumiendo que el evento a no aparece en P , simplemente se reduce a
Ejemplos de
Uno de los ejemplos arquetípicos de CSP es una representación abstracta de una máquina expendedora de chocolate y sus interacciones con una persona que desea comprar chocolate. Esta máquina expendedora podrá realizar dos eventos diferentes, “moneda” y “choc” que representan la inserción del pago y la entrega de un chocolate respectivamente. Una máquina que exige el pago (solo en efectivo) antes de ofrecer un chocolate se puede escribir como:
Una persona que podría optar por utilizar una moneda o una tarjeta para realizar pagos podría modelarse como:
Estos dos procesos se pueden poner en paralelo, para que puedan interactuar entre sí. El comportamiento del proceso compuesto depende de los eventos en los que deben sincronizarse los dos procesos componentes. Por lo tanto,
mientras que si la sincronización solo fuera necesaria en "moneda", obtendríamos
Si abstraemos este último proceso compuesto ocultando los eventos "moneda" y "tarjeta", es decir
obtenemos el proceso no determinista
Este es un proceso que ofrece un evento "choc" y luego se detiene, o simplemente se detiene. En otras palabras, si tratamos la abstracción como una visión externa del sistema (por ejemplo, alguien que no ve la decisión tomada por la persona), se ha introducido el no determinismo .
Definicion formal
Sintaxis
La sintaxis de CSP define las formas "legales" en las que se pueden combinar procesos y eventos. Sea e un evento y X un conjunto de eventos. Entonces, la sintaxis básica de CSP se puede definir como:
Tenga en cuenta que, en aras de la brevedad, la sintaxis presentada anteriormente omite la proceso, que representa divergencia , así como varios operadores, como opciones en paralelo, de tuberías e indexadas alfabéticamente.
Semántica formal
CSP ha sido imbuido 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 , semántica algebraica y semántica operativa mutuamente consistentes .
Semántica denotacional
Los tres modelos denotacionales principales de CSP son el modelo de trazas , el modelo de fallas estables y el modelo de fallas / divergencias . Las asignaciones semánticas de las expresiones de proceso a cada uno de estos tres modelos proporcionan la semántica denotacional para CSP. [1]
El modelo de trazas define el significado de una expresión de proceso como el conjunto de secuencias de eventos (trazas) que se puede observar que realiza el proceso. Por ejemplo,
- desde no realiza eventos
- desde el proceso se puede observar que no se han realizado eventos, el evento a , o la secuencia de eventos a seguido de b
Más formalmente, el significado de un proceso P en el modelo de trazas se define como tal que:
- (es decir contiene la secuencia vacía)
- (es decir es prefijo cerrado)
dónde es el conjunto de todas las posibles secuencias finitas de eventos.
El modelo de fallas estables extiende el modelo de trazas con conjuntos de rechazos, que son conjuntos de eventosque un proceso puede negarse a realizar. Un fracaso es un par, que consta de una traza s , y un conjunto de rechazos X que identifica los eventos que un proceso puede rechazar una vez que ha ejecutado la traza s . El comportamiento observado de un proceso en el modelo de fallas estables es descrito por el par. Por ejemplo,
El modelo de fallas / divergencia amplía aún más el modelo de fallas para manejar la divergencia . La semántica de un proceso en el modelo de fallas / divergencias es un par dónde se define como el conjunto de todos los rastros que pueden conducir a un comportamiento divergente y .
Herramientas
A lo largo de los años, se han producido una serie de herramientas para analizar y comprender los sistemas descritos utilizando CSP. Las primeras implementaciones de herramientas utilizaban una variedad de sintaxis legibles por máquina para CSP, lo que hacía que los archivos de entrada escritos para diferentes herramientas fueran incompatibles. Sin embargo, la mayoría de las herramientas de CSP ahora se han estandarizado con el dialecto legible por máquina de CSP ideado por Bryan Scattergood, a veces referido como CSP M . [17] El dialecto CSP M de CSP posee una semántica operativa definida formalmente , que incluye un lenguaje de programación funcional integrado .
La herramienta CSP más conocida es probablemente Failures / Divergence Refinement 2 ( FDR2 ), que es un producto comercial desarrollado por Formal Systems (Europe) Ltd. FDR2 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 específico (trazas, fallas o fallas / divergencia). [18] FDR2 aplica varios algoritmos de compresión de espacio de estado a los LTS de proceso para reducir el tamaño del espacio de estado que debe explorarse durante una verificación de refinamiento. FDR2 ha sido reemplazado por FDR3, una versión completamente reescrita que incorpora, entre otras cosas, la ejecución paralela y un verificador de tipo integrado. Es lanzado por la Universidad de Oxford, que también lanzó FDR2 en el período 2008-12. [19]
El Adelaide Refinamiento del inspector ( ARC ) [20] es un corrector de CSP refinamiento desarrollada por la formal Modelado y verificación de grupo en 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 explosión de estado de las representaciones LTS explícitas sin requerir el uso de algoritmos de compresión de espacio de estado como los utilizados en FDR2.
El ProB proyecto, [21] que está alojado por el Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, fue creado originalmente para el análisis de apoyo de especificaciones construidas en el método B . Sin embargo, también incluye soporte para el análisis de procesos CSP tanto a través de la verificación de refinamiento como de la verificación del modelo LTL . ProB también se puede utilizar para verificar las propiedades de especificaciones B y CSP combinadas. Un ProBE CSP Animator está integrado en FDR3.
El proceso de análisis Toolkit (PAT) [22] [23] es una herramienta de análisis CSP desarrollado en la Escuela de Computación de la Universidad Nacional de Singapur . PAT puede realizar comprobaciones de refinamiento, comprobaciones de modelos LTL y simulación de procesos CSP y Timed CSP. El lenguaje de proceso PAT extiende CSP con soporte para variables compartidas mutables, paso de mensajes asincrónicos y una variedad de construcciones de procesos relacionados con la equidad y el tiempo cuantitativo como deadline
y waituntil
. El principio de diseño subyacente del lenguaje de proceso 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 de biblioteca C # externa) para una mayor expresividad. Las variables compartidas mutables y los canales asincrónicos proporcionan un azúcar sintáctico conveniente para patrones de modelado de procesos bien conocidos utilizados en CSP estándar. La sintaxis PAT es similar, pero no idéntica, a CSP M . [24] Las principales diferencias entre la sintaxis PAT y CSP M estándar son el uso de punto y coma para terminar expresiones de proceso, la inclusión de azúcar sintáctico para variables y asignaciones, y el uso de sintaxis ligeramente diferente para elección interna y composición paralela.
VisualNets [25] produce visualizaciones animadas de sistemas CSP a partir de especificaciones y admite CSP cronometrado.
CSPsim [26] es un simulador perezoso. No modela CSP de verificación, pero es útil para explorar sistemas muy grandes (potencialmente infinitos).
SyncStitch es un verificador de refinamiento de CSP con modelado interactivo y entorno de análisis. Tiene un editor gráfico de diagramas de transición de estado. El usuario puede modelar el comportamiento de los procesos no solo como expresiones CSP sino también como diagramas de transición de estado. El resultado de la verificación también se informa gráficamente como árboles de cálculo y se puede analizar de forma interactiva con herramientas de inspección periféricas. Además de las comprobaciones de refinamiento, puede realizar una comprobación de interbloqueo y una comprobación de bloqueo activo.
Formalismos relacionados
Varios otros lenguajes de especificación y formalismos se han derivado o inspirado en el clásico CSP sin tiempo, que incluyen:
- CSP temporizado [ enlace muerto permanente ] , que incorpora información de tiempo para razonar sobre sistemas en tiempo real
- Teoría de procesos receptivos , una especialización de CSP que asume una operación de envío asíncrona (es decir, sin bloqueo )
- CSPP
- HCSP
- TCOZ , una integración de Timed CSP y Object Z
- Circus , una integración de CSP y Z basada en las teorías unificadoras de programación
- CML (COMPASS Modeling Language), una combinación de Circus y VDM desarrollada para el modelado de Systems of Systems (SoS)
- CspCASL , una extensión de CASL que integra CSP
- LOTOS , un estándar internacional [27] que incorpora características de CSP y CCS .
- PALPS , una extensión probabilística con ubicaciones para modelos ecológicos desarrollados por Anna Philippou y Mauricio toro bermúdez [ es ]
Comparación con el modelo de actor
En lo que respecta a los procesos concurrentes que intercambian mensajes, el modelo de actor es muy similar a la CSP. Sin embargo, los dos modelos toman algunas decisiones fundamentalmente diferentes con respecto a las primitivas que proporcionan:
- Los procesos de CSP son anónimos, mientras que los actores tienen identidades.
- CSP utiliza canales explícitos para el paso de mensajes, mientras que los sistemas de actores transmiten mensajes a actores de destino nombrados. Estos enfoques pueden considerarse duales entre sí, en el sentido de que los procesos que reciben a través de un solo canal tienen efectivamente una identidad correspondiente a ese canal, mientras que el acoplamiento basado en nombres entre actores puede romperse mediante la construcción de actores que se comportan como canales.
- El paso de mensajes CSP implica fundamentalmente un encuentro entre los procesos involucrados en el envío y la recepción del mensaje, es decir, el remitente no puede transmitir un mensaje hasta que el receptor esté listo para aceptarlo. Por el contrario, el paso de mensajes en los sistemas de actores es fundamentalmente asincrónico, es decir, la transmisión y recepción de mensajes no tienen que suceder al mismo tiempo, y los remitentes pueden transmitir mensajes antes de que los receptores estén listos para aceptarlos. Estos enfoques también pueden considerarse duales entre sí, en el sentido de que los sistemas basados en reuniones pueden usarse para construir comunicaciones en búfer que se comportan como sistemas de mensajería asincrónica, mientras que los sistemas asíncronos pueden usarse para construir comunicaciones de estilo de reunión mediante el uso de un mensaje / Protocolo de reconocimiento para sincronizar remitentes y receptores.
Ver también
- Teoría de los rastros , la teoría general de los rastros.
- Seguimiento de monoide y monoide histórico
- Lenguaje de programación sencillo
- Lenguaje de programación XC
- VerilogCSP es un conjunto de macros agregado a Verilog HDL para admitir la comunicación de comunicaciones de canal de procesos secuenciales.
- Joyce es un lenguaje de programación basado en los principios de CSP, desarrollado por Brinch Hansen alrededor de 1989.
- SuperPascal es un lenguaje de programación también desarrollado por Brinch Hansen , influenciado por CSP y su trabajo anterior con Joyce .
- Ada implementa funciones de CSP como el rendezvous.
- DirectShow es el marco de video dentro de DirectX , utiliza los conceptos de CSP para implementar los filtros de audio y video.
- OpenComRTOS es un RTOS distribuido centrado en la red desarrollado formalmente y basado en un superconjunto pragmático de CSP.
- Autómata de entrada / salida
- Modelo de programación paralela
Referencias
- ↑ a b c d Roscoe, AW (1997). La teoría y práctica de la concurrencia (PDF) . Prentice Hall . ISBN 978-0-13-674409-2.
- ^ Inmos (12 de mayo de 1995). Manual de referencia de occam 2.1 (PDF) . SGS-THOMSON Microelectronics Ltd., Documento INMOS 72 occ 45 03.
- ^ "Recursos sobre programación de subprocesos en el estilo CSP de Bell Labs" . Consultado el 15 de abril de 2010 .
- ^ "Preguntas frecuentes sobre el diseño de lenguajes: ¿Por qué basar la simultaneidad en las ideas de CSP?" .
- ^ "Canales Clojure core.async" .
- ^ a b Hoare, CAR (1978). "Comunicar procesos secuenciales". Comunicaciones de la ACM . 21 (8): 666–677. doi : 10.1145 / 359576.359585 . S2CID 849342 .
- ^ Abdallah, Ali E .; Jones, Cliff B .; Sanders, Jeff W. (2005). Comunicación de procesos secuenciales: los primeros 25 años . LNCS . 3525 . Saltador. ISBN 9783540258131.
- ^ a b Barrett, G. (1995). "Verificación de modelos en la práctica: el procesador de canal virtual T9000". Transacciones IEEE sobre ingeniería de software . 21 (2): 69–78. doi : 10.1109 / 32.345823 .
- ^ a b Hall, A; Chapman, R. (2002). "Corrección por construcción: Desarrollo de un sistema comercial seguro" (PDF) . Software IEEE . 19 (1): 18-25. CiteSeerX 10.1.1.16.1811 . doi : 10.1109 / 52.976937 .
- ^ Creese, S. (2001). Inducción independiente de datos: Verificación del modelo CSP de redes de tamaño arbitrario (= D. Phil.). Universidad de Oxford . CiteSeerX 10.1.1.13.7185 .
- ^ a b Hoare, CAR (1985). Comunicación de procesos secuenciales . Prentice Hall. ISBN 978-0-13-153289-2.
- ^ Clinger, William (junio de 1981). Fundamentos de la semántica del actor (Tesis Doctoral en Matemáticas). MIT. hdl : 1721,1 / 6935 .
- ^ Brookes, Stephen; Hoare, CAR ; Roscoe, AW (1984). "Una teoría de la comunicación de procesos secuenciales". Revista de la ACM . 31 (3): 560–599. doi : 10.1145 / 828.833 . S2CID 488666 .
- ^ Buth, B .; M. Kouvaras; J. Peleska; H. Shi (diciembre de 1997). "Análisis de interbloqueo para un sistema tolerante a fallas". Actas de la 6ª Conferencia Internacional sobre Metodología Algebraica y Tecnología de Software (AMAST'97) . págs. 60–75.
- ^ Buth, B .; J. Peleska; H. Shi (enero de 1999). "Combinación de métodos para el análisis de livelock de un sistema tolerante a fallas". Actas de la 7ma Conferencia Internacional sobre Metodología Algebraica y Tecnología de Software (AMAST'98) . págs. 124-139.
- ^ Lowe, G. (1996). "Rompiendo y arreglando el protocolo de clave pública Needham-Schroeder usando FDR" . Herramientas y Algoritmos para la Construcción y Análisis de Sistemas (TACAS) . Springer-Verlag. págs. 147-166.
- ^ Scattergood, JB (1998). "La semántica y la implementación de CSP legible por máquina". D.Phil. Laboratorio de Computación de la Universidad de Oxford . Cite journal requiere
|journal=
( ayuda ) - ^ AW Roscoe (1994). "CSP de verificación de modelos". En una mente clásica: ensayos en honor a CAR Hoare . Prentice Hall. Cite journal requiere
|journal=
( ayuda ) - ^ "Introducción - documentación FDR 4.2.4" . www.cs.ox.ac.uk .
- ^ Parashkevov, Atanas N .; Yantchev, Jay (1996). "ARC - una herramienta para el refinamiento eficiente y la verificación de equivalencia para CSP". IEEE Int. Conf. sobre algoritmos y arquitecturas para procesamiento en paralelo ICA3PP '96 . págs. 68–75. CiteSeerX 10.1.1.45.3212 .
- ^ Leuschel, Michael; Fontaine, Marc (2008). "Exploración de las profundidades de CSP-M: una nueva herramienta de validación compatible con FDR" (PDF) . ICFEM 2008 . Springer-Verlag. Archivado desde el original (PDF) el 19 de julio de 2011 . Consultado el 26 de noviembre de 2008 .
- ^ Domingo, junio; Liu, Yang; Dong, Jin Song (2009). "PAT: Hacia una verificación flexible bajo la equidad" (PDF) . Actas de la 20ª Conferencia Internacional sobre Verificación Asistida por Computadora (CAV 2009) . Apuntes de conferencias en Ciencias de la Computación. 5643 . Saltador. Archivado desde el original (PDF) el 11 de junio de 2011 . Consultado el 16 de junio de 2009 .
- ^ Domingo, junio; Liu, Yang; Dong, Jin Song (2008). "Model Checking CSP Revisited: Introducing a Process Analysis Toolkit" (PDF) . Actas del Tercer Simposio Internacional sobre Aprovechamiento de Aplicaciones de Métodos Formales, Verificación y Validación (ISoLA 2008) . Comunicaciones en Informática y Ciencias de la Información. 17 . Saltador. págs. 307–322. Archivado desde el original (PDF) el 8 de enero de 2009 . Consultado el 15 de enero de 2009 .
- ^ Domingo, junio; Liu, Yang; Dong, Jin Song; Chen, Chunqing (2009). "Integración de especificaciones y programas para la especificación y verificación del sistema" (PDF) . IEEE Int. Conf. sobre Aspectos Teóricos de la Ingeniería de Software TASE '09 . Archivado desde el original (PDF) el 11 de junio de 2011 . Consultado el 13 de abril de 2009 .
- ^ Green, Mark; Abdallah, Ali (2002). "Análisis de rendimiento y ajuste de comportamiento para la optimización de sistemas de comunicación" . Comunicación de arquitecturas de procesos 2002 .
- ^ Brooke, Phillip; Paige, Richard (2007). "Exploración perezosa y comprobación de modelos CSP con CSPsim". Comunicación de arquitecturas de procesos 2007 .
- ^ ISO 8807, Lenguaje de especificación de orden temporal
Otras lecturas
- Hoare, CAR (2004) [1985]. Comunicación de procesos secuenciales . Prentice Hall International. ISBN 978-0-13-153271-7.
- Este libro ha sido actualizado por Jim Davies en el Laboratorio de Computación de la Universidad de Oxford y la nueva edición está disponible para descargar como archivo PDF en el sitio web Using CSP .
- Roscoe, AW (1997). La teoría y práctica de la concurrencia . Prentice Hall . ISBN 978-0-13-674409-2.
- Algunos enlaces relacionados con este libro están disponibles aquí . El texto completo está disponible para descargar como archivo PS o PDF de la lista de publicaciones académicas de Bill Roscoe .
enlaces externos
- Una versión en PDF del libro CSP de Hoare : se aplican restricciones de derechos de autor; consulte el texto de la página antes de descargar.
- The Annotation of CSP (versión china) Trabajo de traducción y anotación sin fines de lucro basado en el libro de Prentice-Hall (1985), la versión china de Chaochen Zhou (1988) y la versión en línea de Jim Davies (2015).
- WoTUG , un grupo de usuarios para sistemas de estilo CSP y occam, contiene información sobre CSP y enlaces útiles.
- Citas de CSP de CiteSeer