Calculul sistemelor care interacționează
Calculul sistemelor de comunicare ( CCS ) în informatică este un proces de calcul dezvoltat de Robin Milner în 1980. Calculul funcționează cu un model de comunicații inseparabile între exact doi participanți. Limbajul formal include primitive pentru descrierea compoziției paralele, alegerea între acțiuni și cadrele de constrângeri. CCS este util pentru evaluarea corectitudinii calitative a proprietăților precum mutex sau „ livelock ” [1] .
Potrivit lui Milner, „nu este nimic canonic în alegerea combinatoarelor de bază, chiar dacă acestea au fost alese cu mare grijă pentru economie. Ceea ce caracterizează calculul nostru nu este alegerea precisă a combinatorilor, ci alegerea interpretării și a structurii matematice . ”
Expresiile limbajului sunt interpretate ca un sistem tranzitiv etichetat . Între aceste modele , asemănarea reciprocă este folosită ca echivalență semantică.
Sintaxă
Pentru un anumit set de nume de acțiuni, setul de procese CCS este definit de următoarea gramatică Backus-Naur :
![{\displaystyle P::=\emptyset \,\,\,|\,\,\,a.P_{1}\,\,\,|\,\,\,A\,\,\,|\ ,\,\,P_{1}+P_{2}\,\,\,|\,\,\,P_{1}|P_{2}\,\,\,|\,\,\,P_ {1}[b/a]\,\,\,|\,\,\,P_{1}{\backslash }a}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5ead99e00ed96fff0df7c972472973159922c998)
Părți ale sintaxei, în ordinea dată mai sus:
proces gol un proces gol este un proces CCS valid acțiune un proces poate întreprinde o acțiune și poate continua ca proces ID proces scrieți pentru a folosi id pentru a face referire la un proces alegere procesul poate continua fie ca , fie ca compoziție paralelă procese și care există simultan redenumire proces cu acțiuni redenumite în prescripţie proces fără acțiune
![{\displaystyle P_{1}[b/a]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e3845d90265f5e16fb07f1cec4e9d827838f4dad)
Calcul și modele înrudite
- Calculul proceselor care interacționează ( ing. Comunicarea proceselor secvențiale ), CSP este un limbaj dezvoltat de Anthony Hoare , care a apărut în același timp cu CCS.
- Pi-calculus , dezvoltat de Milner la sfârșitul anilor 1980, oferă mobilitate pentru legăturile de comunicare, permițând proceselor să raporteze numele canalelor de comunicare în sine.
- Algebra de proces PEPA , dezvoltată de Jane Hillston , introduce timpul de acțiune și alegerea probabilistică, permițând calcularea valorilor de performanță.
Unele notații bazate pe CCS:
Modele care sunt utilizate în studiul sistemelor CCS:
- Monoid de istorie ;_ _
- Modelul actorului .
Link -uri
- Robin Milner: Un calcul al sistemelor de comunicare , Springer Verlag, ISBN 0-387-10235-3 . 1980.
- Robin Milner, Comunicare și concurență , Prentice Hall, Seria internațională în informatică, ISBN 0-13-115007-3 . 1989
- ↑ Abordarea spațiilor mari de stat în modelarea performanței // Metode formale pentru evaluarea performanței / Herzog, Ulrich. - Springer, 2007. - Vol. 4486. - P. 318-370. — (Note de curs în Informatică). - doi : 10.1007/978-3-540-72522-0 .