Komunikuojantys nuoseklūs procesai

Formali semantika

KNP savyje turi keletą skirtingų formalių semantikų, kurios nusako KNP sintaksės išraiškos reikšmę. KNP teorija apima denotacijos semantiką, algebrinę semantiką ir veiklos semantiką.

Įrankiai

Per keletą paskutinių metų buvo sukrta nemažai įrankių, skirtų analizuoti ir suprasti sistemų aprašymus naudojant CSP. Ankstesnių įrankių realizavimui buvo naudojama mašininės kalbos sintaksė CSP realizavimui, todėl įvesties failai parašyti įvairiomis nesuderinamomis priemonėmis. Tačiau dabar jau dauguma CSP įrankių standartizuoti mašininiam naudojimui. Tai sugalvojo Bryan Scattergood ir šie standartai dar vadinami CSPM. CSPM tai yra BSP formaliai nustatytų procesų veiklos semantika, kurią apima ir apjungia funkcinė programavimo kalba.
Labiausiai žinomi CSP įrankiai yra Failures/Divergence Refinement 2 (FDR2), kuris yra komercinis produktas, sukurtas Formal Systems (Europe) Ltd. FDR2 dažnai yra apibūdinamas kaip modelis tikrintuvas, tačiau tai yra techniškai patobulintas tikrintuvas, nes jis paverčia du CSP procesus išraiškas į Paženklintas Pereinamasias sistemas (LTSs), tada nustato, ar vienas iš procesų, yra kito patobulinimas kai nurodytas semantinis modelis (pėdsakai, gedimai, ar nesėkmės / skirtumai). FDR2 taiko įvairius glaudinimo algoritmus procesui LTSs siekiant sumažinti tyrimo laiką ir reikiamų resursų kiekį, kuri turi būti naudojamas tyrimui pasirinktų procesų.
Adelaide Refinement Checker (ARC) – tai yra CSP patobulintas tikrintuvas, kurį sukūrė Formalių modeliavimų ir tyrimų grupė Adelaidės universitete. ARC skiriasi nuo FDR2, nes viduje yra CSP procesų užsakyti dvejetainės sprendimų diagramas (OBDDs), kurios sumažina vietos užimtumo problemą aiškus LTS atstovavimas reikalauja naudoti vietos glaudinimo algoritmais, tokiais kaip tie, kurie naudojami FDR2.
ProB projektas, kuris yra talpinamas Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, iš pradžių buvo sukurta siekiant remti analizės specifikacijų B metodui. Tačiau palaipsniui jis taip pat suderintas su CSP procesų analizei taip pat ir tikrinimui, bei LTL modelio tikrinimui. ProB taip pat gali būti naudojama patikrinti savybių suderintas CSP ir B aprašymais.
Process Analysis Toolkit (PAT) – tai yra CSP analizės įrankis plėtojamas kompiuterijos mokykloje Nacionaliniame Singapūro universitete. PAT yra pajėgi atlikti patobulintus tikrinimus, LTL modelio tikrinimą ir simuliaciją CSP ir laiko CSP procesus. PAT procesų kalba išplečia CSP suderinimui su skirtingais duomenų tipais, asinchroninis žinutė perdavimas ir teisingumo, bei kiekybiniai laike susiję procesus stabdo, pvz: deadline ir waituntil. Pagrindinis planavimo principas PAT procesų kalboje yra sujungti aukšto lygio programavimo kalbas su procesiniu programvimu (pvz., PAT atveju gali būti nuosekli programa ar net išorės C # biblioteka) geriasniam išraiškingumui. Skitingų kintamųjų tipų dalinimuisi ir asinchroniniais kanalais teikti patogia sintaksine žinomus procesus modeliavimui, modeliuose naudojamas standartas CSP. PAT sintaksė panaši, bet trupti skiriasi nuo CSPM. Pagrindinis skirtumas tarp PAT sintaksės ir CSPM standarto yra kabliataškiai naudojami nutraukti procesus. Integracijoje ir naudojime šiek tiek skiriasi sintaksė vidiniuose pasirinkimuose ir lygiagrečia sudėtimi.
CSPsim tingus simuliatorius. Tai nėra modelis patikrinti CSP, bet tai yra naudinga tiriant labai didelias (galimai begalinias) sistemas.