8. Алгебраические модели систем взаимодействующих процессов. Алгебра процессов - синтаксис. Алгебра процессов - операционная семантика (1265179), страница 2
Текст из файла (страница 2)
Íàðÿäó ñ ââåäåííûì îòíîøåíèåì áèñèìóëÿöèèñóùåñòâóþò è äðóãèå îòíîøåíèÿ ìåæäó ïðîöåññàìè, îòðàæàþùèå áîëüøóþ èëè ìåíüøóþñòåïåíü ñõîæåñòè èõ ïîâåäåíèÿ. Íåêîòîðûå èçýòèõ îòíîøåíèé ìû ðàññìîòðèì äàëåå.2. Âñå ïðîöåññû, êîòîðûå ìîæíî îïðåäåëèòü ïðèïîìîùè ââåäåííûõ âûðàæåíèé àëãåáðû ïðîöåññîâ, èìåþò òîëüêî êîíå÷íûå âû÷èñëåíèÿ.Ïîýòîìó èõ ïðîöåññíûå ãðàôû êîíå÷íû, è èõïîâåäåíèå ëåãêî àíàëèçèðîâàòü.À êàê ìîæíî îïðåäåëèòü ïðîöåññû, èìåþùèåáåñêîíå÷íûå âû÷èñëåíèÿ?ÐåêóðñèÿÅñòü íåñêîëüêî ñïîñîáîâ îïðåäåëåíèÿ ïðîöåññîâ, èìåþùèõíåîãðàíè÷åííî äëèòåëüíûå âû÷èñëåíèÿ.Íàèáîëåå ÷àñòî èñïîëüçóþòñÿ äâà èç íèõ: îïåðàòîððåïëèêàöèè è ðåêóðñèâíûå óðàâíåíèÿ.Îïåðàòîð ðåïëèêàöèè ! â àëãåáðå ïðîöåññîâ ÿâëÿåòñÿ àíàëîãîìîïåðàòîðà èòåðàöèè Êëèíè â àëãåáðå ðåãóëÿðíûõ ìíîæåñòâ.Ñèíòàêñè÷åñêîå îïðåäåëåíèå, ââîäÿùåå îïåðàòîð ðåïëèêàöèèòàêîâî:Iåñëè p ∈ Proc , òî !p ∈ Proc .Ñåìàíòèêà îïåðàòîðà ðåïëèêàöèè îïðåäåëÿåòñÿ òîæäåñòâîìR! : !p ≡ p k!p äëÿ ëþáûõ p ∈ Proc.ÐåêóðñèÿÏðèìåð èñïîëüçîâàíèÿ îïåðàòîðà ðåïëèêàöèè îïèñàíèåñèñòåìû ïåðåäà÷è äàííûõ ïî êàíàëó ñâÿçè ñ ïîäòâåðæäåíèåì:!(send.ack.nil) k!(send.ack.nil)≡ !(send.ack.nil) k send.ack.nil k send.ack.nil k!(send.ack.nil)mes−→ !(send.ack.nil) k ack.nil k ack.nil k!(send.ack.nil)repl−→ !(send.ack.nil) k!(send.ack.nil)ÐåêóðñèÿÄðóãîé, áîëåå îáùèé ñïîñîá îïèñàíèÿ áåñêîíå÷íûõ ïðîöåññîâ îïðåäåëÿòü èõ, êàê ðåøåíèÿ ñèñòåì óðàâíåíèé, ñîäåðæàùèõïðîöåññíûå ïåðåìåííûå.Äîáàâèì ê ìíîæåñòâó èìåí Names ìíîæåñòâî ïðîöåññíûõïåðåìåííûõ X è áóäåì ðàññìàòðèâàòü ïðîöåññíûå âûðàæåíèÿíàä ìíîæåñòâîì áàçîâûõ ñèìâîëîâ Names ∪ X .Òîãäà ðåêóðñèâíîé ñïåöèôèêàöèåé ïðîöåññîâ íàçûâàåòñÿñèñòåìà óðàâíåíèé âèäàX1Xk=Φ1 (X1 , .
. . , Xk )dots=Φk (X1 , . . . , Xk )ãäå X1 , . . . , Xk ïðîöåññíûå ïåðåìåííûå, à Φ1 , . . . , Φk ïðîöåññíûå òåðìû, çàâèñÿùèå òîëüêî îò óêàçàííûõïåðåìåííûõ.ÐåêóðñèÿÍàïðèìåð, ñèñòåìó ïåðåäà÷è äàííûõ ïî êàíàëó ñâçè ñïîäòâåðæäåíèåì ìîæíî îïèñàòü âîò òàêîé ñèñòåìîé óðàâíåíèé:S = X1 k X2X1 = send.ack.nil k X1X2 = send.ack.nil k X2Çàäà÷à.Êàêîâî ðåøåíèå ñëåäóþùåé ñèñòåìû óðàâíåíèéXYZ= Y kZ= a+Z= ā.Z + nilÐåêóðñèÿÎäíàêî íå âñÿêàÿ ñèñòåìà ïðîöåññíûõ óðàâíåíèé èìååòåäèíñòâåííîå ðåøåíèå.Ýòî ìîæíî ãàðàíòèðîâàòü ëèøü äëÿ ïðåäîõðàíÿåìûõ ñèñòåìóðàâíåíèé (guarded recursive specications), ñîñòîÿùèõ èçóðàâíåíèé âèäàXi = a1 .Ψ1 (X1 , . .
. , Xk )+· · ·+am .Ψm (X1 , . . . , Xk )+b1 .nil+· · ·+b` .nil.Çàäà÷à.Íàéäèòå ìåòîä ðåøåíèÿ ëèíåéíûõ ñèñòåì óðàâíåíèé,ñîñòîÿùèõ èç óðàâíåíèé âèäàXi = a1 .Xi1 + · · · + am .Xim + b1 .nil + · · · + b` .nil.ÀáñòðàêöèÿÊîãäà ïðîâîäèòñÿ àíàëèç ïîâåäåíèÿ êàêîé-íèáóäü ñëîæíîéðàñïðåäåëåííîé ñèñòåìû (íàïðèìåð, ìèêðîýëåêòðîííîé ñõåìûèëè îïåðàöèîííîé ñèñòåìû), ìíîãèå äåéñòâèÿ, âûïîëíÿåìûåñèñòåìîé, áûâàþò íåäîñòóïíû äëÿ íàáëþäåíèÿ èëè ïîïðîñòóíåèíòåðåñíû.Òàêèå äåéñòâèÿ ìîæíî ñ÷èòàòü ëèøåííûìè èíäèâèäóàëüíûõîòëè÷èòåëüíûõ ÷åðò, íåîòëè÷èìûìè äðóã îò äðóãà, ñêðûòûìèîò íàáëþäåíèÿ.
Äëÿ èõ îáîçíà÷åíèÿ ââîäèòñÿ ñïåöèàëüíîåñêðûòíîå äåéñòâèå τ .Äëÿ ðàáîòû ñî ñêðûòíûì äåéñòâèåì èñïîëüçóþòñÿ îïåðàöèÿàáñòðàêöèè è îòíîøåíèå âåòâÿùåéñÿ áèñèìóëÿöèè.Àáñòðàêöèÿ ïîçâîëÿåò ñäåëàòü ¾íåâèäèìûìè¿ íåêîòîðûåäåéñòâèÿ ñèñòåìû, à âåòâÿùàÿñÿ áèñèìóëÿöèÿ ïîçâîëÿåòîöåíèâàòü ñõîæåñòü ïîâåäåíèÿ äâóõ ñèñòåì, èãíîðèðóÿ ýòè¾íåâèäèìûìè¿ äåéñòâèÿ.ÀáñòðàêöèÿÎïåðàöèÿ àáñòðàêöèè.Ïóñòü çàäàíî ïðîöåññíîå âûðàæåíèå p è âûäåëåíî íåêîòîðîåïîäìíîæåñòâî âíóòðåííèõ äåéñòâèé I , I ⊆ E .Òîãäà àáñòðàêöèé ïðîöåññà p îòíîñèòåëüíî ìíîæåñòâà Iíàçûâàåòñÿ ïðîöåññ τI (p) , êîòîðûé ïîëó÷àåòñÿ çàìåíîé âïðîöåññå p è âî âñåõ âû÷èñëåíèÿõ ýòîãî ïðîöåññà âñåõ äåéñòâèéèç ìíîæåñòâà I ñêðûòíûì äåéñòâèåì τÍàïðèìåð, åñëè I = {c, e} è ϕ(a) = c , òîτI a.d.nil k ā.e.nil = a.d.nil k ā.τ.nilè âû÷èñëåíèå ïðîöåññà τI (p) èìååò âèäττda.d.nil k ā.τ.nil −→ d.nil k τ.nil −→ d.nil −→ nilÀëãåáðà ïðîöåññîâ: ñèíòàêñèñÑ òî÷êè çðåíèÿ ïîëüçîâàòåëÿ ðàáîòà êîôåéíîé ìàøèíû ýòîàáñòðàêöèÿ åå ïðîöåññà îò íåâèäèìûõ äëÿ ÷åëîâåêà äåéñòâèémake, fill :τ{make,fill} (System) :User k τ{make,fill} (Machine)User= coin.Choice.button.wait.bring .nilChoice = (espresso.nil) + (americano.nil)τ{make,fill} (Machine) = coin.(espresso.nil) + (americano.nil).button.(τ.fill.nil) k fill.bring .nil).nil,ãäå ϕ(fill) = τÂåòâÿùàÿñÿ áèñèìóëÿöèÿÎòíîøåíèå âåòâÿùåéñÿ áèñèìóëÿöèè.Ñèììåòðè÷íîå è ðåôëåêñèâíîå îòíîøåíèåB, B ⊆ Proc × Proc, íàçûâàåòñÿ îòíîøåíèåìâåòâÿùåéñÿ áèñèìóëÿöèè , åñëè îíî óäîâëåòâîðÿåòñëåäóþùåìó òðåáîâàíèþ:xåñëè pBq è p −→p 0 , òî âåðíî îäíî èç äâóõ1.
ëèáî x = τ è p0Bq ,2. ëèáî ñóùåñòâóåò òàêàÿ ïîñëåäîâàòåëüíîñòüïåðåõîäîâ τττxq −→ q1 −→ · · · −→ qn −→ q 0 ,äëÿ êîòîðîé âûïîëíÿþòñÿ îòíîøåíèå p0Bq0 , àòàêæå îòíîøåíèÿ pBqi äëÿ âñåõ i, 1 ≤ i ≤ n .Âåòâÿùàÿñÿ áèñèìóëÿöèÿpyyqÄëÿ ëþáîé ïàðû ïðîöåññîâ p è qÂåòâÿùàÿñÿ áèñèìóëÿöèÿpyByqÄëÿ ëþáîé ïàðû ïðîöåññîâ p è q åñëè pBqÂåòâÿùàÿñÿ áèñèìóëÿöèÿpxp0- yyByqxÄëÿ ëþáîé ïàðû ïðîöåññîâ p è q åñëè pBq è p −→p0,Âåòâÿùàÿñÿ áèñèìóëÿöèÿpτp0- yyBByqxÄëÿ ëþáîé ïàðû ïðîöåññîâ p è q åñëè pBq è p −→p0,ëèáî x = τ è p0BqÂåòâÿùàÿñÿ áèñèìóëÿöèÿpxp0- yyByqτ-yτ-q1r r rτ-yx-qnq åñëè pBqyq0xp −→ p 0 ,Äëÿ ëþáîé ïàðû ïðîöåññîâ p èèëèáî ñóùåñòâóåò òàêàÿ ïîñëåäîâàòåëüíîñòü ïåðåõîäîâÂåòâÿùàÿñÿ áèñèìóëÿöèÿpxp0- yyHHHHByqτ-yτ-q1HHHr r rHHHBHHτ-HHHHyxHqnq0xq åñëè pBq è p −→ p 0 ,yÄëÿ ëþáîé ïàðû ïðîöåññîâ p èëèáî ñóùåñòâóåò òàêàÿ ïîñëåäîâàòåëüíîñòü ïåðåõîäîâäëÿ êîòîðîé p0Bq0,Âåòâÿùàÿñÿ áèñèìóëÿöèÿBpp0y x- yHHHA HHHAHHHHHHAHHHHAH BHBBHAHHHH HHAHHHHAHAHyHy x HτHy τ -Ay τ - r r rqq1qnq åñëè pBqq0xp −→ p 0 ,Äëÿ ëþáîé ïàðû ïðîöåññîâ p èèëèáî ñóùåñòâóåò òàêàÿ ïîñëåäîâàòåëüíîñòü ïåðåõîäîâäëÿ êîòîðîé p0Bq0, à òàêæå pBqi äëÿ âñåõ i, 1 ≤ i ≤ nÂåòâÿùàÿñÿ áèñèìóëÿöèÿÏðèìåðû. îòíîøåíèè âåòâÿùåéñÿ áèñèìóëÿöèè íàõîäÿòñÿïðîöåññû1.
a.nil , τ.a.nil è a.τ.nil2. a.nil + τ.(a.nil + b.nil).nil èτ.(a.nil + b.nil).nil + b.nil3. a.nil + b.nil. è τ.a.nil + b.nilÏî÷åìó?Âåòâÿùàÿñÿ áèñèìóëÿöèÿa.τ.nilaτ.nilτnila.nil B 00yHH00HaτHHBHHH??nilB0HHyyHH00HaHHB 0H BHH?HHyyB0τ.a.nily?a.nily?nilyÂåòâÿùàÿñÿ áèñèìóëÿöèÿÏðèìåðû.Ñëåäóþùèå ïàðû ïðîöåññîâ íå íàõîäÿòñÿ âîòíîøåíèè âåòâÿùåéñÿ áèñèìóëÿöèè:4. a.nil + b.nil è τ.a.nil + b.nil(èíà÷å τ óæå íå áûëî áû ñêðûòíûì äåéñòâèåì îíî ïðèâîäèò ê âûïîëíåíèþ äåéñòâèÿ a , íî íåïðèâîäèò ê âûïîëíåíèþ äåéñòâèÿ b )5.
a.nil + b.nil è τ.a.nil + τ.b.nilÏî÷åìó?Âåòâÿùàÿñÿ áèñèìóëÿöèÿτ.a.nil + b.nilbnilyy@@τ@a.nil+ b.nilyBaa.nilnil@yanily@@BBy@@b@a.nil@yÏðèìåíåíèå àëãåáðû ïðîöåññîâÀëãåáðû ïðîöåññîâ ïðèìåíÿþòñÿ äëÿñïåöèôèêàöèè è âåðèôèêàöèè ðàñïðåäåëåííûõèíôîðìàöèîííûõ ñèñòåì, ñîñòîÿùèõ èçâçàèìîäåéñòâóþùèõ ïðîöåññîâ.Òåõíîëîãèÿ ïðèìåíåíèÿ àëãåáðû ïðîöåññîâòàêîâà.Ïðèìåíåíèå àëãåáðû ïðîöåññîâ1. Òðåáîâàíèÿ, ïðåäúÿâëÿåìûå ê ïðîåêòèðóåìîéðàñïðåäåëåííîé ñèñòåìå, òåõíè÷åñêîå çàäàíèå çàïèñûâàþòñÿ íà îäíîì èç ÿçûêîâ ôîðìàëüíûõ ñïåöèôèêàöèé(íàïðèìåð, íà ÿçûêå îäíîé èç òåìïîðàëüíûõ ëîãèê).Ïîëó÷åííàÿ òàêèì îáðàçîì, ñïåöèôèêàöèÿ Spec èññëåäóåòñÿíà íåïðîòèâîðå÷èâîñòü ïðè ïîìîùè îäíîé èç ñèñòåìàâòîìàòè÷åñêîãî äîêàçàòåëüñòâà òåîðåì.2.
Ìîäåëü ïðîåêòèðóåìîé ðàñïðåäåëåííîé ñèñòåìûîïèñûâàåòñÿ ÿâíî èëè íåÿâíî (ïðè ïîìîùè ïðîöåññíûõóðàâíåíèé Eq ) â àëãåáðå ïðîöåññîâ.Îñíîâíîå âíèìàíèå óäåëÿåòñÿ îïèñàíèþ ïðîòîêîëàâçàèìîäåéñòâèÿ ïðîöåññîâ ïðîåêòèðóåìîé ñèñòåìû.3. Âû÷èñëÿåòñÿ ðåøåíèå p1 , . . . , pN ñèñòåìû ïðîöåññíûõóðàâíåíèé Eq , îïèñûâàþùèõ ïîâåäåíèå ïðîåêòèðóåìîéñèñòåìû, è ñòðîèòñÿ ïàðàëëåëüíàÿ êîìïîçèöèÿModel = p1 k · · · k pN , êîòîðàÿ ïðåäñòàâëÿåò ìîäåëüïðîåêòèðóåìîé ñèñòåìû.Ïðèìåíåíèå àëãåáðû ïðîöåññîâ4.
Ïðîâîäèòñÿ ïðîâåðêà ñîîòâåòñòâèÿ ïîñòðîåííîé ìîäåëèModel çàäàííîé ñïåöèôèêàöèè Spec : Γ(Model) |= Spec .Äëÿ ðåøåíèÿ ýòîé çàäà÷è ïðèìåíÿþòñÿ èíñòðóìåíòûâåðèôèêàöèè ìîäåëåé ïðîãðàìì (model checking).Îáíàðóæåííûå îøèáêè óñòðàíÿþòñÿ çà ñ÷åò óòî÷íåíèÿñïåöèôèêàöèè ïðîåêòà èëè èçìåíåíèÿ ìîäåëè ïðîåêòà.5. Íà îñíîâå ïîñòðîåííîé ìîäåëè Model ñîçäàåòñÿ ïðîãðàììíàÿðåàëèçàöèÿ ïðîåêòèðóåìîé ðàñïðåäåëåííîé ñèñòåìû Prog .Íà êàæäîì ýòàïà ñîçäàíèÿ ðàñïðåäåëåííîé ñèñòåìûIåå ïðîãðàììíàÿ ðåàëèçàöèÿ Prog òðàíñëèðóåòñÿ ââûðàæåíèå àëãåáðû ïðîöåññîâ Syst ,Iê ýòîìó âûðàæåíèþ ïðèìåíÿåòñÿ îïåðàöèÿ àáñòðàêöèèAbstr = τI (Syst) , ñêðûâàþùàÿ âñå íåñóùåñòâåííûåäåéñòâèÿ ïðîöåññà-ðåàëèçàöèè,Iïðîâîäèòñÿ ïðîâåðêà îòíîøåíèÿ âåòâÿùåéñÿ áèñèìóëÿöèèAbstr ∼br Model .Ïðèìåíåíèå àëãåáðû ïðîöåññîâÌàòåìàòè÷åñêàÿ òåîðèÿ ãàðàíòèðóåòΓ(Model) |= Spec ⇔ Γ(Syst) |= Spec.Íî ÷òîáû âîñïîëüçîâàòüñÿ ýòîé òåîðèåé íàäîñïðàâèòüñÿ ñ çàäà÷àìè1.
ðåøåíèÿ ñèñòåì ïðîöåññíûõ óðàâíåíèéEq ⇒ Model ,2. âåðèôèêàöèè ìîäåëåé ïðîãðàììΓ(Model) |= Spec ,3. àáñòðàêöèè ïðîãðàììProg ⇒ Syst ⇒ Abstr = τI (Syst) ,4. ïðîâåðêè áèñèìóëÿöèîííîé ýêâèâàëåíòíîñòèAbstr ∼br Model .ÊÎÍÅÖ ËÅÊÖÈÈ 8.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
