b'\n_START_ARTICLE_\nKomunikuojantys nuosekl\xc5\xabs procesai\n_START_SECTION_\nFormali semantika\n_START_PARAGRAPH_\nKNP savyje turi kelet\xc4\x85 skirting\xc5\xb3 formali\xc5\xb3 semantik\xc5\xb3, kurios nusako KNP sintaks\xc4\x97s i\xc5\xa1rai\xc5\xa1kos reik\xc5\xa1m\xc4\x99. KNP teorija apima denotacijos semantik\xc4\x85, algebrin\xc4\x99 semantik\xc4\x85 ir veiklos semantik\xc4\x85.\n_START_SECTION_\n\xc4\xaerankiai\n_START_PARAGRAPH_\nPer kelet\xc4\x85 paskutini\xc5\xb3 met\xc5\xb3 buvo sukrta nema\xc5\xbeai \xc4\xafranki\xc5\xb3, skirt\xc5\xb3 analizuoti ir suprasti sistem\xc5\xb3 apra\xc5\xa1ymus naudojant CSP. Ankstesni\xc5\xb3 \xc4\xafranki\xc5\xb3 realizavimui buvo naudojama ma\xc5\xa1inin\xc4\x97s kalbos sintaks\xc4\x97 CSP realizavimui, tod\xc4\x97l \xc4\xafvesties failai para\xc5\xa1yti \xc4\xafvairiomis nesuderinamomis priemon\xc4\x97mis. Ta\xc4\x8diau dabar jau dauguma CSP \xc4\xafranki\xc5\xb3 standartizuoti ma\xc5\xa1ininiam naudojimui. Tai sugalvojo Bryan Scattergood ir \xc5\xa1ie standartai dar vadinami CSPM. CSPM tai yra BSP formaliai nustatyt\xc5\xb3 proces\xc5\xb3 veiklos semantika, kuri\xc4\x85 apima ir apjungia funkcin\xc4\x97 programavimo kalba._NEWLINE_Labiausiai \xc5\xbeinomi CSP \xc4\xafrankiai yra Failures/Divergence Refinement 2 (FDR2), kuris yra komercinis produktas, sukurtas Formal Systems (Europe) Ltd. FDR2 da\xc5\xbenai yra apib\xc5\xabdinamas kaip modelis tikrintuvas, ta\xc4\x8diau tai yra techni\xc5\xa1kai patobulintas tikrintuvas, nes jis paver\xc4\x8dia du CSP procesus i\xc5\xa1rai\xc5\xa1kas \xc4\xaf Pa\xc5\xbeenklintas Pereinamasias sistemas (LTSs), tada nustato, ar vienas i\xc5\xa1 proces\xc5\xb3, yra kito patobulinimas kai nurodytas semantinis modelis (p\xc4\x97dsakai, gedimai, ar nes\xc4\x97km\xc4\x97s / skirtumai). FDR2 taiko \xc4\xafvairius glaudinimo algoritmus procesui LTSs siekiant suma\xc5\xbeinti tyrimo laik\xc4\x85 ir reikiam\xc5\xb3 resurs\xc5\xb3 kiek\xc4\xaf, kuri turi b\xc5\xabti naudojamas tyrimui pasirinkt\xc5\xb3 proces\xc5\xb3._NEWLINE_Adelaide Refinement Checker (ARC) \xe2\x80\x93 tai yra CSP patobulintas tikrintuvas, kur\xc4\xaf suk\xc5\xabr\xc4\x97 Formali\xc5\xb3 modeliavim\xc5\xb3 ir tyrim\xc5\xb3 grup\xc4\x97 Adelaid\xc4\x97s universitete. ARC skiriasi nuo FDR2, nes viduje yra CSP proces\xc5\xb3 u\xc5\xbesakyti dvejetain\xc4\x97s sprendim\xc5\xb3 diagramas (OBDDs), kurios suma\xc5\xbeina vietos u\xc5\xbeimtumo problem\xc4\x85 ai\xc5\xa1kus LTS atstovavimas reikalauja naudoti vietos glaudinimo algoritmais, tokiais kaip tie, kurie naudojami FDR2._NEWLINE_ProB projektas, kuris yra talpinamas Institut f\xc3\xbcr Informatik, Heinrich-Heine-Universit\xc3\xa4t D\xc3\xbcsseldorf, i\xc5\xa1 prad\xc5\xbei\xc5\xb3 buvo sukurta siekiant remti analiz\xc4\x97s specifikacij\xc5\xb3 B metodui. Ta\xc4\x8diau palaipsniui jis taip pat suderintas su CSP proces\xc5\xb3 analizei taip pat ir tikrinimui, bei LTL modelio tikrinimui. ProB taip pat gali b\xc5\xabti naudojama patikrinti savybi\xc5\xb3 suderintas CSP ir B apra\xc5\xa1ymais._NEWLINE_Process Analysis Toolkit (PAT) \xe2\x80\x93 tai yra CSP analiz\xc4\x97s \xc4\xafrankis pl\xc4\x97tojamas kompiuterijos mokykloje Nacionaliniame Singap\xc5\xabro universitete. PAT yra paj\xc4\x97gi atlikti patobulintus tikrinimus, LTL modelio tikrinim\xc4\x85 ir simuliacij\xc4\x85 CSP ir laiko CSP procesus. PAT proces\xc5\xb3 kalba i\xc5\xa1ple\xc4\x8dia CSP suderinimui su skirtingais duomen\xc5\xb3 tipais, asinchroninis \xc5\xbeinut\xc4\x97 perdavimas ir teisingumo, bei kiekybiniai laike susij\xc4\x99 procesus stabdo, pvz: deadline ir waituntil. Pagrindinis planavimo principas PAT proces\xc5\xb3 kalboje yra sujungti auk\xc5\xa1to lygio programavimo kalbas su procesiniu programvimu (pvz., PAT atveju gali b\xc5\xabti nuosekli programa ar net i\xc5\xa1or\xc4\x97s C # biblioteka) geriasniam i\xc5\xa1rai\xc5\xa1kingumui. Skiting\xc5\xb3 kintam\xc5\xb3j\xc5\xb3 tip\xc5\xb3 dalinimuisi ir asinchroniniais kanalais teikti patogia sintaksine \xc5\xbeinomus procesus modeliavimui, modeliuose naudojamas standartas CSP. PAT sintaks\xc4\x97 pana\xc5\xa1i, bet trupti skiriasi nuo CSPM. Pagrindinis skirtumas tarp PAT sintaks\xc4\x97s ir CSPM standarto yra kabliata\xc5\xa1kiai naudojami nutraukti procesus. Integracijoje ir naudojime \xc5\xa1iek tiek skiriasi sintaks\xc4\x97 vidiniuose pasirinkimuose ir lygiagre\xc4\x8dia sud\xc4\x97timi._NEWLINE_CSPsim tingus simuliatorius. Tai n\xc4\x97ra modelis patikrinti CSP, bet tai yra naudinga tiriant labai didelias (galimai begalinias) sistemas.'