Rachunek systemów komunikujących się - Calculus of communicating systems

Rachunek systemów komunikujących ( CCS ) jest rachunek proces wprowadzony przez Robin Milner około 1980 roku i tytuł książki opisującej rachunku. Jego działania modelują niepodzielną komunikację między dokładnie dwoma uczestnikami. Język formalny zawiera prymitywy opisujące kompozycję równoległą, wybór między działaniami i ograniczenie zakresu. CCS jest przydatny do oceny jakościowej poprawności właściwości systemu, takiego jak zakleszczenia lub livelock .

Według Milnera „Nie ma nic kanonicznego w wyborze podstawowych kombinatorów, mimo że zostały one wybrane z wielką dbałością o ekonomię. To, co charakteryzuje nasz rachunek, to nie dokładny wybór kombinatorów, ale raczej wybór interpretacji i ram matematycznych. ”.

Wyrażenia języka są interpretowane jako oznakowany system przejściowy . Pomiędzy tymi modelami bispodobieństwo jest używane jako równoważność semantyczna.

Składnia

Mając zestaw nazw akcji, zestaw procesów CCS jest zdefiniowany przez następującą gramatykę BNF :

${\displaystyle P::=0\,\,\,|\,\,\,a.P_{1}\,\,\,|\,\,\,A\,\,\,|\, \,\,P_{1}+P_{2}\,\,\,|\,\,\,P_{1}|P_{2}\,\,\,|\,\,\,P_{ 1}[b/a]\,\,\,|\,\,\,P_{1}{\backslash }a\,\,\,}$

Części składni są w kolejności podanej powyżej

nieaktywny proces

nieaktywny proces jest prawidłowym procesem CCS${\ Displaystyle 0}$

akcja

proces może wykonać akcję i kontynuować jako proces${\displaystyle a.P_{1}}$${\displaystyle a}$${\displaystyle P_{1}}$

identyfikator procesu

napisz, aby użyć identyfikatora do odwoływania się do procesu (który może zawierać sam identyfikator , tj. dozwolone są definicje rekurencyjne)${\ Displaystyle A {\ overset {\ underset {\ operatorname {def}} {}} {=}} P_ {1}}$${\ Displaystyle A}$${\displaystyle P_{1}}$${\ Displaystyle A}$

wybór

proces może przebiegać jako proces lub proces${\displaystyle P_{1}+P_{2}}$${\displaystyle P_{1}}$${\displaystyle P_{2}}$

kompozycja równoległa

${\displaystyle P_{1}|P_{2}}$mówi, że procesy i istnieją jednocześnie${\displaystyle P_{1}}$${\displaystyle P_{2}}$

zmiana nazwy

${\displaystyle P_{1}[b/a]}$to proces ze wszystkimi akcjami nazwanymi przemianowanymi na${\displaystyle P_{1}}$${\displaystyle a}$${\displaystyle b}$

ograniczenie

${\ Displaystyle P_ {1} {\ ukośnik odwrotny} a}$jest proces bez działania${\displaystyle P_{1}}$${\displaystyle a}$

Powiązane rachunki, modele i języki

• Komunikowanie się procesów sekwencyjnych (CSP), opracowane przez Tony'ego Hoare'a , jest językiem formalnym, który powstał w podobnym czasie co CCS.
• Algebra procesów Komunikowanie (ACP) został opracowany przez Jana Bergstra i Jan Willem Klop w 1982 roku, i używa aksjomatyczną podejście (w stylu algebry uniwersalnej ) do rozumu o podobnej klasy procesów jak CCS.
• Pi-rachunek , opracowany przez Robin Milner , Joachim Parrow i Davida Walkera w późnych latach 80-tych rozciąga CCS z mobilnością łączy komunikacyjnych, pozwalając procesy komunikowania nazwiska samych kanałów komunikacji.
• PEPA , opracowany przez Jane Hillston, wprowadza synchronizację aktywności pod względem wykładniczo rozłożonych stawek i wyboru probabilistycznego, umożliwiając ocenę wskaźników wydajności.
• Reversible Communicating Concurrent Systems (RCCS) wprowadzony przez Vincenta Danosa , Jeana Krivine'a i innych, wprowadza (częściową) odwracalność w realizacji procesów CCS.

Niektóre inne języki oparte na CCS:

• Rachunek systemów nadawczych
• Język specyfikacji zamówień czasowych (LOTOS)
• Process Calculus for Spatally-Explicit Ecological Models (PALPS) jest rozszerzeniem CCS z probabilistycznym wyborem, lokalizacjami i atrybutami lokalizacji
• Silnik interpretera języka orkiestracji Java (Jolie)

Modele, które zostały wykorzystane w badaniu systemów podobnych do CCS:

• Monoid historii
• Model aktora

Bibliografia

• Robin Milner: rachunek systemów komunikacyjnych , Springer Verlag, ISBN  0-387-10235-3 . 1980.
• Robin Milner, Komunikacja i współbieżność , Prentice Hall, International Series in Computer Science, ISBN  0-13-115007-3 . 1989