Kölcsönható rendszerek számítása
A számítástechnikában a kommunikációs rendszerek kalkulusa ( CCS ) egy Robin Milner által 1980-ban kifejlesztett folyamatszámítás . A kalkulus pontosan két résztvevő közötti elválaszthatatlan kommunikáció modelljével működik. A formális nyelv primitíveket tartalmaz a párhuzamos kompozíció, a cselekvések közötti választás és a kényszer keretek leírására. A CCS hasznos az olyan tulajdonságok minőségi helyességének értékelésére, mint a mutex vagy a " livelock " [1] .
Milner szerint „semmi kanonikus az alapkombinátorok megválasztásában, annak ellenére, hogy a gazdaságosság szempontjából nagy körültekintéssel választották ki őket. Számításunkat nem a kombinátorok pontos megválasztása jellemzi, hanem az értelmezés és a matematikai szerkezet megválasztása . ”
A nyelvi kifejezéseket címkézett tranzitív rendszerként értelmezzük . E modellek között a kölcsönös hasonlóságot szemantikai ekvivalenciaként használják.
Szintaxis
Adott műveletnevek készletéhez a CCS-folyamatok halmazát a következő Backus-Naur nyelvtan határozza meg :
![{\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)
A szintaxis részei, a fent megadott sorrendben:
üres folyamat egy üres folyamat érvényes CCS-folyamat akció egy folyamat cselekvést hajthat végre és folyamatként folytatódhat folyamatazonosító írjon , hogy az id -t használja egy folyamatra való hivatkozáshoz választás a folyamat folytatódhat mint , vagy mint párhuzamos összetétel folyamatok és amelyek egyszerre léteznek átnevezése folyamat a következőre átnevezett műveletekkel korlátozás cselekvés nélküli folyamat
![{\displaystyle P_{1}[b/a]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e3845d90265f5e16fb07f1cec4e9d827838f4dad)
Kapcsolódó kalkulusok és modellek
- A CSP egy Anthony Hoare általkifejlesztett nyelv , amely a CCS-sel egy időben jelent meg.
- A Milner által az 1980-as évek végén kifejlesztett Pi-calculus mobilitást biztosít a kommunikációs kapcsolatok számára azáltal, hogy lehetővé teszi a folyamatok számára, hogy maguknak a kommunikációs csatornáknak a nevét jelentsék.
- A Jane Hillston által kifejlesztett PEPA folyamatalgebra bevezeti a cselekvési időt és a valószínűségi választást, lehetővé téve a teljesítménymutatók kiszámítását.
Néhány CCS-en alapuló jelölés:
A CCS-rendszerek tanulmányozására használt modellek:
- Történeti monoid ;_ _
- A színész modell .
Linkek
- Robin Milner: A kommunikációs rendszerek számítása , Springer Verlag, ISBN 0-387-10235-3 . 1980.
- Robin Milner, Kommunikáció és párhuzamosság , Prentice Hall, Számítástechnikai nemzetközi sorozat, ISBN 0-13-115007-3 . 1989
- ↑ Nagy állapotterek kezelése a teljesítménymodellezésben // Formal Methods for Performance Evaluation / Herzog, Ulrich. - Springer, 2007. - Vol. 4486. - P. 318-370. — (Számítástechnikai előadásjegyzetek). - doi : 10.1007/978-3-540-72522-0 .