Počet interagujících systémů
Calculus of Communicating Systems ( CCS ) v počítačové vědě je procesní počet vyvinutý Robinem Milnerem v roce 1980. Kalkulus pracuje s modelem neoddělitelné komunikace právě dvou účastníků. Formální jazyk zahrnuje primitiva pro popis paralelní kompozice, volbu mezi akcemi a omezující rámce. CCS je užitečné pro hodnocení kvalitativní správnosti vlastností, jako je mutex nebo " livelock " [1] .
Podle Milnera „na volbě základních kombinátorů není nic kanonického, přestože byly vybrány s velkou péčí o hospodárnost. To, co charakterizuje náš kalkul, není přesná volba kombinátorů, ale volba interpretace a matematické struktury .
Jazykové výrazy jsou interpretovány jako označený tranzitivní systém . Mezi těmito modely se používá vzájemná podobnost jako sémantická ekvivalence.
Syntaxe
Pro danou sadu názvů akcí je sada procesů CCS definována následující gramatikou Backus-Naur :
![{\displaystyle P::=\emptyset \,\,\,|\,\,\,a.P_{1}\,\,\,|\,\,\,A\,\,\,|\ ,\,\,P_{1}+P_{2}\,\,\,|\,\,\,P_{1}|P_{2}\,\,\,|\,\,\,P_ {1}[b/a]\,\,\,|\,\,\,P_{1}{\obrácené lomítko }a}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5ead99e00ed96fff0df7c972472973159922c998)
Části syntaxe ve výše uvedeném pořadí:
prázdný proces prázdný proces je platný proces CCS akce proces může provést akci a pokračovat jako proces ID procesu zápis použít id k odkazování na proces výběr proces může pokračovat buď jako , nebo jako paralelní složení procesy a které existují současně přejmenování proces s akcemi přejmenovanými na omezení proces bez akce
![{\displaystyle P_{1}[b/a]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e3845d90265f5e16fb07f1cec4e9d827838f4dad)
Související výpočty a modely
- Počet interagujících procesů ( angl. Communicating sekvenční procesy ), CSP je jazyk vyvinutý Anthonym Hoareem , který se objevil ve stejné době jako CCS.
- Pi-calculus , vyvinutý Milnerem na konci 80. let, poskytuje mobilitu pro komunikační spojení tím, že umožňuje procesům hlásit názvy komunikačních kanálů samy.
- Procesní algebra PEPA , kterou vyvinula Jane Hillston , zavádí dobu akce a pravděpodobnostní volbu, což umožňuje vypočítat metriky výkonu.
Některé zápisy založené na CCS:
Modely, které se používají při studiu systémů CCS:
- Historie monoidní ;_ _
- Herecký model .
Odkazy
- Robin Milner: A Calculus of Communicating Systems , Springer Verlag, ISBN 0-387-10235-3 . 1980.
- Robin Milner, Communication and Concurrency , Prentice Hall, International Series in Computer Science, ISBN 0-13-115007-3 . 1989
- ↑ Řešení velkých stavových prostorů v modelování výkonu // Formální metody pro hodnocení výkonu / Herzog, Ulrich. - Springer, 2007. - Sv. 4486. - S. 318-370. — (Poznámky z informatiky). - doi : 10.1007/978-3-540-72522-0 .