Komunikuojantys nuoseklūs procesai

Straipsnis iš Vikipedijos, laisvosios enciklopedijos.
Jump to navigation Jump to search
 Broom icon.svg  Šį puslapį ar jo dalį reikia sutvarkyti pagal Vikipedijos standartus.
Jei galite, sutvarkykite.

Sintaksė[redaguoti | redaguoti vikitekstą]

KNP (Komunikuojantys nuoseklūs procesai) sintaksė nusako galimus būdus, kaip procesai ir įvykiai gali būti tarpusavyje sujungti. Tegul būna įvikis, o sąrašas įvykių. Tada KNP sintaksė gali būti nusakoma kaip:


Atkreipkite dėmesį į sintaksės glaustumą. Šita pateikta sintaksė neparodo proceso, kuris nurodo nuokrypį, kaip ir skirtingos operacijos tokios kaip, jungimas (angl. "piping") ar indeksuotas pasirinkimas (angl. "indexed choices").


Formali semantika[redaguoti | redaguoti vikitekstą]

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ą.

Denotacijos semantika[redaguoti | redaguoti vikitekstą]

Trys pagrindinės KNP denotacijos modeliai yra: žymių modelis, pastovių nesėkmių modelis ir nesekmių/skirtumų modelis. Semantiniai jungimai tarp procesų išraiškų ir tarp šių trijų modelių duoda mums denotacijos KNP semantiką.

Žymių modelis nusako proceso išraiškos reikšmę kaip sąrašą įvykių, kur galima stebėti proceso veikimą. Pavyzdžiui:

  • nuo nesukuria įvykio
  • nuo proceso gali būti stebimas veikimas kuris nesukuria įvykio, įvykis , seka įvykių sekama

Daugiau formali proceso reikšmė žymių modelyje yra nusakoma kaip:

kaip:

  1. (pvz.: turi tuščia seką)
  2. (pvz.: )

Čia yra baigtinis sąrašas visų galimų įvykių sekų.

Stabilių nesėkmių modelis paveldi žymių modelį su atmestu sąrašu, kuris yra įvikių sąrašas jame procesas gali atsisakyti veikti. Nesekmė yra pora , kuriame žymė yra: ir atsisakantis veikti sąrašas . Tame sąraše yra indentifikuojami įvykiai kurie gali atsisakyti veikti, kai jie bus paleisti. Stabilių nesėkmių modelyje procesas yra stebimas kaip pora math>\left(traces\left(P\right), failures\left(P\right)\right)</math> pavyzdžiui:


Nesėkmių/nuokrypių modelis toliau paveldi nesėkmių modelį, kad galėtų kontroliuoti nuokripį. Nesėkmių/nuokrypių modelyje procesas yra pora kur yra nusakomas kaip sąrašas visų įmanomų žymių, kurie gali turėti skirtingą "elgesį" .

 Broom icon.svg  Šį puslapį ar jo dalį reikia sutvarkyti pagal Vikipedijos standartus.
Jei galite, sutvarkykite.

Įrankiai[redaguoti | redaguoti vikitekstą]

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.