Szekvenciális folyamatok kommunikálása - Communicating sequential processes

A számítástechnika , a kommunikáció szekvenciális folyamatok ( CSP ) egy formális nyelvet leírására minták az interakció a konkurens rendszerek . Ez egy családtag matematikai elméletek konkurencia ismert folyamat algebra, vagy folyamat calculi alapuló üzenet halad keresztül csatornákat . A CSP nagy hatással volt az occam programozási nyelv kialakítására, és befolyásolta a programozási nyelvek, például a Limbo , a RaftLib , a Go , a Crystal és a Clojure core.async tervezését is.

A CSP -t először Tony Hoare 1978 -as cikkében írták le , de azóta jelentősen fejlődött. A CSP -t gyakorlatilag alkalmazták az iparban, mint eszközt a különböző rendszerek, például a T9000 Transputer , valamint a biztonságos e -kereskedelmi rendszer egyidejű szempontjainak meghatározására és ellenőrzésére . Maga a CSP elmélete továbbra is aktív kutatás tárgyát képezi, beleértve a gyakorlati alkalmazhatóság körének növelését célzó munkát (pl. A traktálhatóan elemezhető rendszerek skálájának növelése).

Történelem

A Hoare eredeti, 1978 -as cikkében bemutatott CSP -verzió lényegében párhuzamos programozási nyelv volt, nem pedig folyamatszámítás . Lényegében más szintaxissal rendelkezett, mint a CSP későbbi verziói, nem rendelkezett matematikailag meghatározott szemantikával, és képtelen volt képviselni a korlátlan nem determinizmust . A programokat az eredeti CSP-ben rögzített számú szekvenciális folyamat párhuzamos összetételeként írták, amelyek szigorúan szinkron üzenetátvitel útján kommunikálnak egymással. A CSP későbbi verzióival ellentétben minden folyamathoz explicit nevet rendeltek, és az üzenet forrását vagy célját a tervezett küldési vagy fogadási folyamat nevének megadásával határozták meg. Például a folyamat

COPY = *[c:character; west?c → east!c]

ismételten kap egy karaktert a megnevezett folyamatból, westés elküldi azt a megnevezett folyamatnak east. A párhuzamos összetétel

[west::DISASSEMBLE || X::COPY || east::ASSEMBLE]

hozzárendeli a neveket westa DISASSEMBLEfolyamathoz, Xa COPYfolyamathoz és easta ASSEMBLEfolyamathoz, és végrehajtja ezt a három folyamatot egyidejűleg.

A CSP eredeti verziójának közzétételét követően Hoare, Stephen Brookes és AW Roscoe kifejlesztette és finomította a CSP elméletét modern, folyamatalgebrai formájába. A CSP folyamatalgebrává fejlesztésének módját Robin Milner kommunikációs rendszerek számításával (CCS) kapcsolatos munkája befolyásolta, és fordítva. A CSP elméleti változatát eredetileg Brookes, Hoare és Roscoe 1984-es cikkében mutatták be, majd Hoare 1985-ben megjelent Communications Sequential Processes című könyvében . 2006 szeptemberében ez a könyv még mindig a harmadik legtöbbet idézett informatika volt. minden idők referenciája Citeseer szerint (bár mintavételének jellege miatt megbízhatatlan forrás). A CSP elmélete néhány kisebb változtatáson ment keresztül Hoare könyvének megjelenése óta. A legtöbb ilyen változást a CSP folyamatelemzéséhez és ellenőrzéséhez használt automatizált eszközök megjelenése motiválta. Roscoe Az egyidejűség elmélete és gyakorlata a CSP ezen újabb verzióját írja le.

Alkalmazások

A CSP egyik korai és fontos alkalmazása az INMOS T9000 Transputer , egy összetett szuperskaláris csővezetékes processzor elemeinek specifikációjára és ellenőrzésére való felhasználása volt , amelyet nagyméretű többprocesszoros feldolgozás támogatására terveztek. A CSP-t a processzorcső és a virtuális csatornaprocesszor helyességének ellenőrzésére használták, amelyek a processzoron kívüli kommunikációt kezelték.

A CSP ipari felhasználása a szoftvertervezéshez általában a megbízható és biztonságkritikus rendszerekre összpontosít. Például a Brémai Biztonságos Rendszerek Intézete és a Daimler-Benz Aerospace modellezte a CSP Nemzetközi Űrállomáson való használatra szánt hibakezelő rendszert és avionikai interfészt (körülbelül 23 000 kódsorból áll), és elemezte a modellt annak megerősítésére, hogy kialakításuk mentes volt a patthelyzettől és az életszagtól. A modellezési és elemzési folyamat számos olyan hibát tudott feltárni, amelyeket egyedül a teszteléssel nehéz lett volna észlelni. Hasonlóképpen, a Praxis High Integrity Systems alkalmazta a CSP modellezést és elemzést a szoftver (kb. 100 000 soros kód) fejlesztése során egy biztonságos intelligens kártya tanúsító hatóság számára annak érdekében, hogy ellenőrizze, hogy a tervezésük biztonságos és holtpont nélküli. A Praxis azt állítja, hogy a rendszer sokkal alacsonyabb hibaaránnyal rendelkezik, mint a hasonló rendszerek.

Mivel a CSP jól alkalmazható olyan rendszerek modellezésére és elemzésére, amelyek komplex üzenetváltást tartalmaznak, a kommunikációs és biztonsági protokollok ellenőrzésére is alkalmazták. Az ilyen típusú alkalmazások kiemelkedő példája, hogy Lowe a CSP-t és az FDR finomító-ellenőrzőt használja a Needham – Schroeder nyilvános kulcsú hitelesítési protokoll elleni korábban ismeretlen támadás felfedezésére, majd a támadás leküzdésére alkalmas, javított protokoll kifejlesztésére.

Informális leírás

Ahogy a neve is sugallja, a CSP lehetővé teszi a rendszerek leírását olyan komponens folyamatok alapján, amelyek egymástól függetlenül működnek, és egymással kölcsönhatásba lépnek, kizárólag üzenettovábbító kommunikáció révén. A CSP név "szekvenciális" része azonban ma már téves megnevezés, mivel a modern CSP lehetővé teszi az alkatrészfolyamatok meghatározását mind szekvenciális folyamatként, mind pedig primitívebb folyamatok párhuzamos összetételeként. A különböző folyamatok közötti kapcsolatokat és az egyes folyamatok környezetével való kommunikációját különböző folyamatalgebrai operátorok segítségével írják le . Ezzel az algebrai megközelítéssel meglehetősen bonyolult folyamatleírásokat lehet könnyen összeállítani néhány primitív elemből.

Primitívek

A CSP két primitív osztályt biztosít a folyamatalgebrájában:

Események

Az események kommunikációt vagy interakciót jelentenek. Feltételezzük, hogy oszthatatlanok és pillanatok. Lehetnek atomi neveket (pl szóló , off ), összetett nevek (pl valve.open , valve.close ), vagy a bemeneti / kimeneti események (pl egér? Xy , képernyőn! Bitmap ).

Primitív folyamatok

A primitív folyamatok alapvető viselkedést képviselnek: példák közé tartozik a STOP (a semmit nem kommunikáló folyamat, más néven holtpont ), és a SKIP (ami sikeres befejezést jelent).

Algebrai operátorok

A CSP számos algebrai operátorral rendelkezik. A legfontosabbak a következők:

Előtag

Az előtag -operátor egyesíti az eseményt és a folyamatot, hogy új folyamatot hozzon létre. Például,

${\ displaystyle a \ to P}$

az a folyamat, hogy hajlandó kommunikálni a környezetével, és miután egy , viselkedik a folyamat P .

Determinista választás

A determinisztikus (vagy külső) választási operátor lehetővé teszi egy folyamat jövőbeli fejlődését, mint két komponenses folyamat közötti választást, és lehetővé teszi a környezet számára, hogy az egyik folyamat kezdeti eseményének közlésével megoldja a választást. Például,

${\ displaystyle (a \ - P) \ Box (b \ - Q)}$

az a folyamat, amely hajlandó közölni az a és b kezdeti eseményeket, majd ezt követően P vagy Q néven viselkedik , attól függően, hogy a környezet melyik kezdeti eseményt választja közölni. Ha az a és a b egyidejűleg kommunikálna, a választás nem determinisztikus módon megoldódna.

Nem determinisztikus választás

A nem determinisztikus (vagy belső) választási operátor lehetővé teszi egy folyamat jövőbeli fejlődésének meghatározását, mint két komponenses folyamat közötti választást, de nem teszi lehetővé a környezet számára azt a szabályozást, amely felett az egyik komponens folyamat kiválasztásra kerül. Például,

${\ displaystyle (a \ - P) \ sqcap (b \ Q)}$

viselkedhet úgy, mint vagy . Ez nem hajlandók elfogadni egy vagy b , és csak akkor kell kommunikálni, ha a környezet egyaránt kínál egy és b . A non -determinismust akaratlanul is be lehet vezetni egy névlegesen determinisztikus választásba, ha a választás mindkét oldalának kezdeti eseményei azonosak. Tehát például${\ displaystyle (a \ - P)}$${\ displaystyle (b \ Q)}$

${\ displaystyle (a \ to a \ to {\ text {STOP}}) \ Box (a \ to b \ to {\ text {STOP}})}$

egyenértékű

${\ displaystyle a \ to {\ big (} (a \ to {\ text {STOP}}) \ sqcap (b \ to {\ text {STOP}}) {\ big)}}$

Összeszövés

Az átlapoló operátor teljesen független párhuzamos tevékenységet képvisel. A folyamat

${\ displaystyle P \; ||| \; Q}$

egyszerre viselkedik P -ként és Q -ként . Mindkét folyamat eseményei időben tetszőlegesen összefűződnek.

Interfész párhuzamos

Az interfész párhuzamos operátor egyidejű tevékenységet képvisel, amely szinkronizálást igényel az alkatrészfolyamatok között: az interfészkészlet bármely eseménye csak akkor fordulhat elő, ha az összes komponens folyamat képes részt venni az adott eseményben. Például a folyamat

${\ displaystyle P \; | [\ {a \}] | \; Q}$

megköveteli, hogy P és Q egyaránt képes legyen az a esemény végrehajtására , mielőtt az esemény bekövetkezhetne. Tehát például a folyamat

${\ displaystyle (a \ - P) \; | [\ {a \}] | \; (a \ Q)}$

részt vehet a eseményben , és a folyamatgá válhat

${\ displaystyle P \; | [\ {a \}] | \; Q}$

míg

${\ displaystyle (a \ - P) \; | [\ {a, b \}] | \; (b \ Q)}$

egyszerűen holtpontra kerül.

Rejtőzik

A rejtőzködő operátor lehetőséget biztosít a folyamatok absztrakciójára azáltal, hogy bizonyos eseményeket megfigyelhetetlenné tesz. A rejtőzködés triviális példája az

${\ displaystyle (a \ - P) \ setminus \ {a \}}$

elő, feltételezve, hogy az esemény egy nem jelenik meg a P , egyszerűen csökkenti a

${\ displaystyle P}$

Példák

Az egyik archetipikus CSP -példa egy csokoládé -automata absztrakt ábrázolása, és annak kölcsönhatása egy csokoládét vásárolni kívánó személlyel. Ez az automata képes lehet két különböző esemény lebonyolítására, az „érme” és a „csoki”, amelyek a fizetés behelyezését és a csokoládé kiszállítását jelentik. Az a gép, amely fizetést igényel (csak készpénzben) a csokoládé felajánlása előtt, a következőképpen írható:

${\ displaystyle \ mathrm {VendingMachine} = \ mathrm {coin} \ rightarrow \ mathrm {choc} \ rightarrow \ mathrm {STOP}}$

Az a személy, aki esetleg érmét vagy kártyát használ a fizetéshez, a következőképpen modellezhető:

${\ displaystyle \ mathrm {Person} = (\ mathrm {coin} \ rightarrow \ mathrm {STOP}) \ Box (\ mathrm {card} \ rightarrow \ mathrm {STOP})}$

Ez a két folyamat párhuzamba állítható, hogy kölcsönhatásba léphessenek egymással. Az összetett folyamat viselkedése az eseményektől függ, amelyeken a két komponens folyamatnak szinkronizálnia kell. És így,

${\ displaystyle \ mathrm {VendingMachine} \ left \ vert \ left [\ left \ {\ mathrm {coin}, \ mathrm {card} \ right \} \ right] \ right \ vert \ mathrm {Person} \ equiv \ mathrm {coin} \ rightarrow \ mathrm {choc} \ rightarrow \ mathrm {STOP}}$

mivel ha a szinkronizálásra csak az „érmén” lenne szükség, akkor megkapnánk

${\ displaystyle \ mathrm {VendingMachine} \ left \ vert \ left [\ left \ {\ mathrm {coin} \ right \} \ right] \ right \ vert \ mathrm {Person} \ equiv \ left (\ mathrm {coin} \ rightarrow \ mathrm {choc} \ rightarrow \ mathrm {STOP} \ right) \ Box \ left (\ mathrm {card} \ rightarrow \ mathrm {STOP} \ right)}$

Ha ezt az utóbbi összetett folyamatot úgy vonjuk el, hogy elrejtjük az „érme” és a „kártya” eseményeket, pl

${\ displaystyle \ left (\ left (\ mathrm {coin} \ rightarrow \ mathrm {choc} \ rightarrow \ mathrm {STOP} \ right) \ Box \ left (\ mathrm {card} \ rightarrow \ mathrm {STOP} \ right ) \ jobb) \ setminus \ left \ {\ mathrm {érme, kártya} \ jobb \}}$

megkapjuk a nem determinisztikus folyamatot

${\ displaystyle \ left (\ mathrm {choc} \ rightarrow \ mathrm {STOP} \ right) \ sqcap \ mathrm {STOP}}$

Ez egy folyamat, amely vagy felajánl egy „choc” eseményt, majd leáll, vagy csak leáll. Más szóval, ha az absztrakciót a rendszer külső nézeteként kezeljük (pl. Valaki, aki nem látja az adott személy által hozott döntést), akkor a nemdeterminizmus lépett életbe .

Formális meghatározás

Szintaxis

A CSP szintaxisa meghatározza a folyamatok és események kombinálásának „törvényes” módjait. Legyen e esemény, X pedig események halmaza. Ezután a CSP alapvető szintaxisa a következőképpen határozható meg:

${\ displaystyle {\ begin {array} {lcll} {Proc} & :: = & \ mathrm {STOP} & \; \\ & | & \ mathrm {SKIP} & \; \\ & | & e \ rightarrow {Proc } & ({\ text {előtag}}}) \\ & | & {Proc} \; \ Box \; {Proc} & ({\ text {external}} \; {\ text {choice}}) \\ & | & {Proc} \; \ sqcap \; {Proc} & ({\ text {nondeterministic}} \; {\ text {choice}}) \\ & | & {Proc} \; \ vert \ vert \ vert \ ; {Proc} & ({\ text {interleaving}}) \\ & | & {Proc} \; | [\ {X \}] | \; {Proc} & ({\ text {interface}}} \; { \ text {parallel}}) \\ & | & {Proc} \ setminus X & ({\ text {hiding}}) \\ & | & {Proc}; {Proc} & ({\ text {sequential}} \; {\ text {összetétel}}) \\ & | & \ mathrm {if} \; b \; \ mathrm {then} \; {Proc} \; \ mathrm {else} \; Proc & ({\ text {boolean} } \; {\ text {feltételes}}) \\ & | & {Proc} \; \ triangleright \; {Proc} & ({\ text {timeout}}) \\ & | & {Proc} \; \ háromszög \; {Proc} & ({\ text {interrupt}}) \ end {tömb}}}$

Vegye figyelembe, hogy a rövidség kedvéért a fent bemutatott szintaxis kihagyja az eltérést jelentő folyamatot, valamint a különböző operátorokat, például az ábécé szerinti párhuzamot, a csövezést és az indexelt választásokat. ${\ displaystyle \ mathbf {div}}$

Formális szemantika

CSP lett átitatva különböző formális szemantika , amely meghatározza a jelentését a szintaktikailag helyes CSP kifejezéseket. A CSP elmélete kölcsönösen következetes denotációs szemantikát , algebrai szemantikát és operatív szemantikát foglal magában .

Denotációs szemantika

A CSP három fő denotációs modellje a nyomkövetési modell, a stabil hibamodell és a hibák/divergenciák modell. A folyamatkifejezésekről e három modell mindegyikére vonatkozó szemantikai leképezések biztosítják a CSP denotációs szemantikáját.

A nyomkövetési modell egy folyamatkifejezés jelentését az események (nyomok) sorozataként határozza meg, amelyek végrehajtását megfigyelhetjük. Például,

• ${\ displaystyle \ mathrm {traces} \ left (\ mathrm {STOP} \ right) = \ left \ {\ langle \ rangle \ right \}}$mivel nem hajt végre eseményeket${\ displaystyle \ mathrm {STOP}}$
• ${\ displaystyle \ mathrm {traces} \ left (a \ rightarrow b \ rightarrow \ mathrm {STOP} \ right) = \ left \ {\ langle \ rangle, \ langle a \ rangle, \ langle a, b \ rangle \ right \}}$mivel az eljárás is megfigyelhető, hogy végre nincs esemény, az esemény egy , vagy az események sorozata egy , majd b${\ displaystyle (a \ rightarrow b \ rightarrow \ mathrm {STOP})}$

Formálisabban a P folyamat jelentését a nyomkövetési modellben úgy határozzuk meg , hogy: ${\ displaystyle \ mathrm {traces} \ left (P \ right) \ subseteq \ Sigma ^{\ ast}}$

1. ${\ displaystyle \ langle \ rangle \ in \ mathrm {traces} \ left (P \ right)}$(azaz az üres sorozatot tartalmazza)${\ displaystyle \ mathrm {traces} \ bal (P \ jobb)}$
2. ${\ displaystyle s_ {1} \ smallfrown s_ {2} \ in \ mathrm {traces} \ left (P \ right) \ azt jelenti, hogy s_ {1} \ in \ mathrm {traces} \ bal (P \ jobb)}$(azaz előtag zárva van)${\ displaystyle \ mathrm {traces} \ bal (P \ jobb)}$

hol van az összes lehetséges véges eseménysor halmaza. ${\ displaystyle \ Sigma ^{\ ast}}$

A stabil hibamodell kiterjeszti a nyomkövetési modellt elutasító halmazokkal, amelyek olyan eseményhalmazok, amelyeket egy folyamat megtagadhat. A hiba egy pár , amely egy s nyomból és egy X elutasító halmazból áll, amelyek azonosítják azokat az eseményeket, amelyeket egy folyamat megtagadhat, miután végrehajtotta az s nyomkövetést . A folyamat megfigyelt viselkedését a stabil hibamodellben a pár írja le . Például, ${\ displaystyle X \ subseteq \ Sigma}$${\ displaystyle \ left (s, X \ right)}$${\ displaystyle \ left (\ mathrm {traces} \ bal (P \ jobb), \ mathrm {kudarcok} \ balra (P \ jobb) \ jobb)}$

• ${\ displaystyle \ mathrm {kudarcok} \ left (\ left (a \ rightarrow \ mathrm {STOP} \ right) \ Box \ left (b \ rightarrow \ mathrm {STOP} \ right) \ right) = \ left \ {\ bal (\ langle \ rangle, \ emptyyset \ right), \ left (\ langle a \ rangle, \ left \ {a, b \ right \} \ right), \ left (\ langle b \ rangle, \ left \ { a, b \ jobb \} \ jobb) \ jobb \}}$
• ${\ displaystyle \ mathrm {kudarcok} \ left (\ left (a \ rightarrow \ mathrm {STOP} \ right) \ sqcap \ left (b \ rightarrow \ mathrm {STOP} \ right) \ right) = \ left \ {\ bal (\ langle \ rangle, \ left \ {a \ right \} \ right), \ left (\ langle \ rangle, \ left \ {b \ right \} \ right), \ left (\ langle a \ rangle, \ bal \ {a, b \ jobb \} \ jobb), \ bal (\ langle b \ rangle, \ bal \ {a, b \ jobb \} \ jobb) \ jobb \}}$

A hibák/divergencia modell tovább bővíti a hibamodellt a divergencia kezelésére . A folyamat szemantikája a kudarcok/divergenciák modellben olyan pár, ahol az összes nyom halmazaként van definiálva, amelyek divergens viselkedéshez vezethetnek és . ${\ displaystyle \ bal (\ mathrm {kudarcok} _ {{perp} \ bal (P \ jobb), \ mathrm {divergences} \ bal (P \ jobb) \ jobb)}$${\ displaystyle \ mathrm {divergences} \ bal (P \ jobb)}$${\ displaystyle \ mathrm {kudarcok} _ {\ perp} \ balra (P \ jobbra) = \ mathrm {kudarcok} \ balra (P \ jobbra) \ csésze \ balra \ {\ balra (k, X \ jobbra) \ közép s \ in \ mathrm {divergences} \ bal (P \ jobb) \ jobb \}}$

Eszközök

Az évek során számos eszköz készült a CSP segítségével leírt rendszerek elemzésére és megértésére. A korai szerszám implementációk számos gépi olvasható szintaxist használtak a CSP-hez, így a különböző eszközökhöz írt bemeneti fájlok összeférhetetlenné váltak. Azonban a legtöbb CSP-eszköz mára a Bryan Scattergood által kidolgozott CSP géppel olvasható nyelvjárására szabványosult, amelyet néha CSP _M-nek is neveznek . A CSP CSP _M dialektusa formálisan meghatározott működési szemantikával rendelkezik , amely egy beágyazott funkcionális programozási nyelvet is tartalmaz .

A legismertebb CSP-eszköz valószínűleg a Failures/Divergence Refinement 2 ( FDR2 ), amely a Formal Systems (Europe) Ltd. által kifejlesztett kereskedelmi termék. Az FDR2-t gyakran modell-ellenőrzőként írják le , de technikailag finomítás- ellenőrző. két CSP folyamatkifejezést átalakít címkézett átmeneti rendszerekké (LTS), majd meghatározza, hogy az egyik folyamat a másik finomítása -e valamely meghatározott szemantikai modellben (nyomok, kudarcok vagy kudarcok/eltérések). Az FDR2 különféle állapot-tér tömörítési algoritmusokat alkalmaz a folyamat LTS-ekre annak érdekében, hogy csökkentse az állapot-tér méretét, amelyet feltárni kell a finomítás ellenőrzése során. Az FDR2 utódja az FDR3, egy teljesen átírt verzió, amely többek között párhuzamos végrehajtást és integrált típusellenőrzőt tartalmaz. Az Oxfordi Egyetem adja ki, amely szintén kiadta az FDR2-t a 2008-12 közötti időszakban.

Az Adelaide Refinement Checker ( ARC ) egy CSP finomító ellenőrző, amelyet az Adelaide -i Egyetem Formális Modellezési és Verifikációs Csoportja fejlesztett ki . Az ARC abban különbözik az FDR2-től, hogy a CSP-folyamatokat belsőleg rendezett bináris döntési diagramokként (OBDD) képviseli, ami enyhíti az explicit LTS-ábrázolások állapotrobbanás-problémáját anélkül, hogy megkövetelné az FDR2-ben használt állapot-tér tömörítési algoritmusok használatát.

A ProB projekt, amelynek a Heinrich-Heine-Universität Düsseldorf Institut für Informatik ad otthont, eredetileg a B módszerrel felépített specifikációk elemzésének támogatására jött létre . Ez azonban magában foglalja a CSP-folyamatok elemzésének támogatását mind finomítás, mind pedig LTL- modell-ellenőrzés révén. A ProB használható a kombinált CSP és B specifikációk tulajdonságainak ellenőrzésére is. A ProBE CSP Animator integrálva van az FDR3 -ba.

A Process Analysis Toolkit (PAT) egy CSP elemző eszköz, amelyet a Szingapúri Nemzeti Egyetem Számítástechnikai Iskolájában fejlesztettek ki . A PAT képes finomítási ellenőrzést, LTL modell-ellenőrzést, valamint a CSP és az időzített CSP folyamatok szimulációját. A PAT folyamatnyelv kiterjeszti a CSP -t, támogatva a megváltoztatható megosztott változókat, az aszinkron üzenetátadást, valamint a különböző méltányossági és mennyiségi időfüggő folyamatkonstrukciókat, például deadlineés waituntil. A PAT folyamatnyelv alapvető tervezési elve az, hogy a magas szintű specifikációs nyelvet kombinálja az eljárási programokkal (pl. Egy esemény a PAT-ban lehet szekvenciális program vagy akár külső C# könyvtárhívás) a nagyobb kifejezőképesség érdekében. A megváltoztatható megosztott változók és az aszinkron csatornák kényelmes szintaktikai cukrot biztosítanak a szabványos CSP-ben használt jól ismert folyamatmodellezési mintákhoz. A PAT szintaxisa hasonló, de nem azonos a CSP _{M -vel} . A fő különbségek a PAT szintaxis és a standard CSP _M között a pontosvesszők használata a folyamatkifejezések befejezésére, a szintaktikai cukor beépítése a változókhoz és a hozzárendelésekhez, valamint a kissé eltérő szintaxis használata a belső választás és a párhuzamos összetétel érdekében.

A VisualNets a specifikációk alapján animált vizualizációt készít a CSP -rendszerekről, és támogatja az időzített CSP -t .

A CSPsim egy lusta szimulátor. Nem modellezi az CSP -t, de hasznos nagyon nagy (potenciálisan végtelen) rendszerek feltárásához.

A SyncStitch egy CSP -s finomítás -ellenőrző interaktív modellezési és elemzési környezettel. Grafikus állapotátmenet diagram szerkesztővel rendelkezik. A felhasználó a folyamatok viselkedését nemcsak CSP-kifejezésekként, hanem állapotátmeneti diagramként is modellezheti. Az ellenőrzés eredményét grafikusan számítási faként is jelentik, és perifériás ellenőrző eszközökkel interaktívan elemezhetők. A finomítási ellenőrzéseken kívül holtpont -ellenőrzést és éleszár -ellenőrzést is végezhet.

Kapcsolódó formalizmusok

Számos más specifikációs nyelv és formalizmus származik a klasszikus időzített CSP -ből, vagy ihlette őket, többek között:

• Időzített CSP , amely időzítési információkat tartalmaz a valós idejű rendszerekről való érveléshez
• Receptive Process Theory , a CSP specializációja, amely aszinkron (azaz nem blokkoló ) küldési műveletet feltételez
• CSPP
• HCSP
• TCOZ , az időzített CSP és a Z objektum integrációja
• Circus , integrációs CSP és Z alapuló Unifying elméletei programozás
• CML (COMPASS Modeling Language), a Circus és a VDM kombinációja, amelyet rendszerek rendszereinek (SoS) modellezésére fejlesztettek ki
• CspCASL , a CASL kiterjesztése, amely integrálja a CSP -t
• A LOTOS nemzetközi szabvány, amely magában foglalja a CSP és a CCS funkcióit .
• PALPS , egy valószínű kiterjesztés az Anna Philippou és Mauricio toro bermúdez által kifejlesztett ökológiai modellek helyszíneivel

Összehasonlítás a színész modellel

Amennyire az egyidejű üzeneteket cserélő folyamatokról van szó, a szereplőmodell nagyjából hasonlít a CSP -hez. A két modell azonban alapvetően eltérő döntéseket hoz az általuk nyújtott primitívek tekintetében:

• A CSP folyamatok névtelenek, míg a szereplők identitással rendelkeznek.
• A CSP explicit csatornákat használ az üzenetek továbbítására, míg a színészrendszerek üzeneteket továbbítanak a megnevezett célszereplőknek. Ezeket a megközelítéseket egymás kettősének lehet tekinteni, abban az értelemben, hogy az egyetlen csatornán keresztül érkező folyamatok gyakorlatilag az adott csatornának megfelelő identitással rendelkeznek, míg a szereplők közötti névalapú kapcsolat megszakadhat csatornákként viselkedő szereplők felépítésével.
• A CSP üzenettovábbítás alapvetően egy találkozót foglal magában az üzenet küldésében és fogadásában részt vevő folyamatok között, azaz a feladó nem tud üzenetet továbbítani, amíg a fogadó készen áll az elfogadásra. Ezzel szemben az üzenetátadás a szereplőrendszerekben alapvetően aszinkron, azaz az üzenetküldésnek és -fogadásnak nem kell egyszerre történnie, és a feladók továbbíthatnak üzeneteket, mielőtt a vevők készen állnak az elfogadásra. Ezeket a megközelítéseket egymás kettősének is tekinthetjük, abban az értelemben, hogy a randevúalapú rendszerek pufferelt kommunikáció létrehozására használhatók, amelyek aszinkron üzenetküldő rendszerekként viselkednek, míg az aszinkron rendszerek találkozási stílusú kommunikáció létrehozására használhatók üzenet használatával/ nyugtázó protokoll a küldők és fogadók szinkronizálásához.

Díj

1990 -ben „egy királynő díja a technológiai eredményekért ... az [Oxfordi Egyetem] Számítási Laboratóriumában . A díj elismeri a sikeres együttműködést a laboratórium és az Inmos Kft. Között . Az Inmos zászlóshajója a „ transzuter ”, egy mikroprocesszor, amely számos olyan alkatrésszel rendelkezik, amelyekre általában szükség lenne ugyanazon egyetlen komponens beépítésével . ” Tony Hoare szerint: „Az INMOS Transputer megtestesítője volt az olyan mikroprocesszorok létrehozásának ötleteinek, amelyek képesek kommunikálni egymással a vezetékek között húzódó vezetékek mentén. Az alapítónak az volt az elképzelése, hogy a CSP -ötletek megéretek az ipari hasznosításra, és ő hozta létre a Transputers programozásának nyelvét, amelyet Occam -nak hívtak . … A vállalat becslése szerint lehetővé tette számukra a hardver leszállítását egy évvel korábban, mint egyébként. Az Oxfordi Egyetem Számítási Laboratóriumával közösen pályáztak és elnyerték a Queen díját a technológiai eredményekért. ”

Lásd még

• Nyomelmélet , a nyomok általános elmélete.
• Nyomkövetési monoid és történelem monoid
• Egyszerű programozási nyelv
• XC programozási nyelv
• VerilogCSP egy sor makrók adunk Verilog HDL a támogatási kommunikáló szekvenciális folyamatok csatorna kommunikáció.
• A Joyce a CSP elvein alapuló programozási nyelv, amelyet Brinch Hansen fejlesztett ki 1989 körül.
• A SuperPascal egy programozási nyelv, amelyet szintén Brinch Hansen fejlesztett ki , és amelyet a CSP és Joyce -val végzett korábbi munkái befolyásoltak .
• Az Ada megvalósítja a CSP funkcióit, például a találkozót.
• A DirectShow a DirectX -en belüli videókeret , a CSP -koncepciókat használja az audio- és videószűrők megvalósításához.
• Az OpenComRTOS egy hivatalosan kifejlesztett hálózatközpontú elosztott RTOS, amely a CSP pragmatikus szuperszettjén alapul.
• Bemeneti/kimeneti automata
• Párhuzamos programozási modell

Hivatkozások

További irodalom

• Hoare, CAR (2004) [1985]. Szekvenciális folyamatok kommunikálása . Prentice Hall International. ISBN 978-0-13-153271-7.
  • Ezt a könyvet Jim Davies frissítette az Oxfordi Egyetem Számítási Laboratóriumában, és az új kiadás letölthető PDF -fájlként a CSP használata webhelyen.
• Roscoe, AW (1997). Az egyidejűség elmélete és gyakorlata . Prentice Hall . ISBN 978-0-13-674409-2.
  • A könyvhöz kapcsolódó néhány link itt érhető el . A teljes szöveg letölthető PS vagy PDF fájlként Bill Roscoe tudományos publikációinak listájáról .

Külső linkek

• A Hoare CSP könyvének PDF verziója - Szerzői jogi korlátozás érvényes, nézze meg az oldal szövegét letöltés előtt.
• The Annotation of CSP (Chinese Version) Nonprofit fordító és jegyzetelő munka a Prentice-Hall könyv (1985), Chaochen Zhou kínai verziója (1988) és Jim Davies online verziója (2015) alapján.
• A WoTUG , a CSP és occam stílusú rendszerek felhasználói csoportja tartalmaz néhány információt a CSP -ről és hasznos linkeket.
• CSP idézetek a CiteSeer -től