Cálculo de sistemas que interactúan
El Cálculo de Sistemas de Comunicación ( CCS ) en informática es un proceso de cálculo desarrollado por Robin Milner en 1980. El cálculo funciona con un modelo de comunicaciones inseparables entre exactamente dos participantes. El lenguaje formal incluye primitivas para describir la composición paralela, la elección entre acciones y marcos de restricción. CCS es útil para evaluar la corrección cualitativa de propiedades como mutex o " livelock " [1] .
Según Milner, “no hay nada canónico en la elección de los combinadores básicos, aunque hayan sido elegidos con mucho cuidado por la economía. Lo que caracteriza a nuestro cálculo no es la elección precisa de combinadores, sino la elección de interpretación y estructura matemática . ”
Las expresiones lingüísticas se interpretan como un sistema transitivo etiquetado . Entre estos modelos , la similitud mutua se utiliza como equivalencia semántica.
Sintaxis
Para un conjunto dado de nombres de acción, el conjunto de procesos CCS se define mediante la siguiente gramática de Backus-Naur :
![{\displaystyle P::=\emptyset \,\,\,|\,\,\,a.P_{1}\,\,\,|\,\,\,A\,\,\,|\ ,\,\,P_{1}+P_{2}\,\,\,|\,\,\,P_{1}|P_{2}\,\,\,|\,\,\,P_ {1}[b/a]\,\,\,|\,\,\,P_{1}{\barra invertida}a}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5ead99e00ed96fff0df7c972472973159922c998)
Partes de la sintaxis, en el orden indicado anteriormente:
proceso vacío un proceso vacío es un proceso CCS válido acción un proceso puede tomar una acción y continuar como un proceso identificacion de proceso escribir para usar id para referirse a un proceso elección el proceso puede continuar como , o como composición paralela procesos y que existen simultáneamente renombrar proceso con acciones renombradas a limitación proceso sin acción
![{\displaystyle P_{1}[b/a]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e3845d90265f5e16fb07f1cec4e9d827838f4dad)
Cálculo y modelos relacionados
- Cálculo de procesos interactivos ( ing. Comunicación de procesos secuenciales ), CSP es un lenguaje desarrollado por Anthony Hoare , que apareció al mismo tiempo que CCS.
- Pi-calculus , desarrollado por Milner a fines de la década de 1980, proporciona movilidad para los enlaces de comunicación al permitir que los procesos informen los nombres de los propios canales de comunicación.
- El álgebra de procesos PEPA , desarrollado por Jane Hillston , introduce el tiempo de acción y la elección probabilística, lo que permite calcular las métricas de rendimiento.
Algunas notaciones basadas en CCS:
Modelos que se utilizan en el estudio de los sistemas CCS:
- Monoide de historia ;_ _
- El actor modelo .
Enlaces
- Robin Milner: un cálculo de sistemas de comunicación , Springer Verlag, ISBN 0-387-10235-3 . 1980.
- Robin Milner, Comunicación y concurrencia , Prentice Hall, Serie internacional en informática, ISBN 0-13-115007-3 . 1989
- ↑ Abordar grandes espacios de estado en el modelado de rendimiento // Métodos formales para la evaluación del rendimiento / Herzog, Ulrich. - Springer, 2007. - Vol. 4486. - Pág. 318-370. — (Apuntes de clase en informática). -doi : 10.1007 / 978-3-540-72522-0 .