Лекция 6. Символьный алгоритм верификации моделей для CTL (1185528), страница 3
Текст из файла (страница 3)
×òîáûñôîðìóëèðîâàòü ñèìâîëüíûé àëãîðèòì âåðèôèêàöèè ìîäåëåé,ëó÷øå âñåãî èñïîëüçîâàòü ñîêðàùåííóþ ñèñòåìó îáîçíà÷àíèéäëÿ ñëîæíûõ îïåðàöèé íà áóëåâûõ ôîðìóëàõ. Äëÿ ýòîãîïðèãîäíû êâàíòèôèöèðîâàííûå áóëåâû ôîðìóëû (QBF).state explosion¾êîìáèíàòîðíîãî âçðûâà¿ ÷èñëà ñîñòîÿíèéÑèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÏóñòü çàäàíî ìíîæåñòâî V = {v0, . . . , vn−1}ïðîïîçèöèîíàëüíûõ ïåðåìåííûõ. Îáîçíà÷èì ÷åðåç QBF(V )íàèìåíüøåå ìíîæåñòâî ôîðìóë, óäîâëåòâîðÿþùèõ ñëåäóþùèìóñëîâèÿì:I êàæäàÿ ïåðåìåííàÿ èç V ÿâëÿåòñÿ ôîðìóëîé;I åñëè f è g ôîðìóëû, òî ôîðìóëàìè ÿâëÿþòñÿ èâûðàæåíèÿ ¬f , f ∧ g , f ∨ g ;I åñëè f ôîðìóëà è v ∈ V , òî ôîðìóëàìè ÿâëÿþòñÿ èâûðàæåíèÿ ∃v f è ∀v f .Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÎöåíêîé çíà÷åíèé èñòèííîñòè äëÿ ìíîæåñòâà QBF(V )íàçûâàåòñÿ ôóíêöèÿ σ : V → {0, 1} .
Åñëè a ∈ {0, 1} , òî çàïèñüσhv ← ai îáîçíà÷àåò èñòèííîñòíóþ îöåíêó, êîòîðîåîïðåäåëÿåòñÿ ñëåäóþùèìñîîòíîøåíèåì:a , åñëè v = w ,σhv ← ai(w ) =σ(w ) , åñëè v 6= w .Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÎöåíêîé çíà÷åíèé èñòèííîñòè äëÿ ìíîæåñòâà QBF(V )íàçûâàåòñÿ ôóíêöèÿ σ : V → {0, 1} . Åñëè a ∈ {0, 1} , òî çàïèñüσhv ← ai îáîçíà÷àåò èñòèííîñòíóþ îöåíêó, êîòîðîåîïðåäåëÿåòñÿ ñëåäóþùèìñîîòíîøåíèåì:a , åñëè v = w ,σhv ← ai(w ) =σ(w ) , åñëè v 6= w .Çàïèñü σ |= f , ãäå f êâàíòèôèöèðîâàííàÿ áóëåâà ôîðìóëà, àσ èñòèííîñòíàÿ îöåíêà, îáçíà÷àåò, ÷òî ôîðìóëà f èñòèííàïðè îöåíêå σ .
Îòíîøåíèå |= îïðåäåëÿåòñÿ èíäóêòèâíîî÷åâèäíûì îáðàçîì:Iσ |= v ⇐⇒ σ(v ) = 1,Iσ |= ¬fIσ |= f ∨ g ⇐⇒ σ |= fIII⇐⇒ σ 6|= f ,èëè σ |= g ,σ |= f ∧ g ⇐⇒ σ |= f è σ |= g ,σ |= ∃vf ⇐⇒ σhv → 0i |= f èëè σhv → 1i |= f ,σ |= ∀vf ⇐⇒ σhv → 0i |= f è σhv → 1i |= f .Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÂûðàçèòåëüíûå âîçìîæíîñòè QBF òî÷íî òàêèå æå, êàê è óîáû÷íûõ áóëåâûõ ôîðìóë, ïðîñòî QBF áîëåå ëàêîíè÷íû.Êàæäàÿ QBF çàäàåò íåêîòîðîå îòíîøåíèå íà ìíîæåñòâå V , èýòî îòíîøåíèå ìîæíî ðåàëèçîâàòü ïðè ïîìîùè ROBDD, åñëèâîñïîëüçîâàòüñÿ êîìïîçèöèåé îïåðàöèè îãðàíè÷åíèÿ èîïåðàöèè Apply :I ∃xf = f |x←0 ∨ f |x←1 ,I ∀xf = f |x←0 ∧ f |x←1 .Êâàíòîðû èñïîëüçóþòñÿ ïðåèìóùåñòâåííî â îïåðàöèÿõðåëÿöèîííîãî ïðîèçâåäåíèÿ , êîòîðûå ìîæíî ïðåäñòàâèòü ââèäå ∃v [f (w , v ) ∧ g (v , x)] .Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÑèìâîëüíûé àëãîðèòì âåðèôèêàöèè ìîäåëåé ðåàëèçîâàí ââèäå ïðîöåäóðû Check .
Îíà ïîëó÷àåò â êà÷åñòâå àðãóìåíòàCTL ôîðìóëó ϕ , êîòîðóþ íåîáõîäèìî ïðîâåðèòü, è OBDD,ïðåäñòàâëÿþùåé îòíîøåíèå ïåðåõîäîâ R àíàëèçèðóåìîéìîäåëè Êðèïêå M . Ïðîöåäóðà âû÷èñëÿåò OBDD,ïðåäñòàâëÿþùóþ ìíîæåñòâî Sϕ = {s | M, s |= ϕ} âñåõ òåõñîñòîÿíèé ìîäåëè M , â êîòîðûõ âûïîëíÿåòñÿ ϕ .Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÑèìâîëüíûé àëãîðèòì âåðèôèêàöèè ìîäåëåé ðåàëèçîâàí ââèäå ïðîöåäóðû Check . Îíà ïîëó÷àåò â êà÷åñòâå àðãóìåíòàCTL ôîðìóëó ϕ , êîòîðóþ íåîáõîäèìî ïðîâåðèòü, è OBDD,ïðåäñòàâëÿþùåé îòíîøåíèå ïåðåõîäîâ R àíàëèçèðóåìîéìîäåëè Êðèïêå M . Ïðîöåäóðà âû÷èñëÿåò OBDD,ïðåäñòàâëÿþùóþ ìíîæåñòâî Sϕ = {s | M, s |= ϕ} âñåõ òåõñîñòîÿíèé ìîäåëè M , â êîòîðûõ âûïîëíÿåòñÿ ϕ .Ïðîöåäóðà Check ïðîâîäèò âû÷èñëåíèÿ èíäóêòèâíî, ñîîáðàçíîñòðóêòóðå CTL ôîðìóë.Åñëè f ýòî àòîìàðíîå âûñêàçûâàíèå a , òî Check(f , R) ýòîOBDD, ïðåäñòàâëÿþùàÿ ìíîæåñòâî ñîñòîÿíèé ñèñòåìû, âêîòîðûõ âûïîëíÿåòñÿ a .Åñëè f = f1 ∨ f2 èëè f = ¬f1 , òî Check(f , R) ïîëó÷àåòñÿïðèìåíåíèåì ôóíêöèè Apply ê àðãóìåíòàì Check(f1, R) èCheck(f2 , R) .Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÔîðìóëû âèäà f , [f g ] èïîìîùè îòäåëüíûõ ïðîöåäóðEXEUEGfîáðàáàòûâàþòñÿ ïðèCheck(EX f , R) = CheckEX (Check(f , R))Check(E[fU,g ], R) = CheckEU(Check(f , R), Check(g , R))Check(EG f , R) = CheckEG (Check(f , R)).,Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÔîðìóëû âèäà f , [f g ] èïîìîùè îòäåëüíûõ ïðîöåäóðEXEUEGfîáðàáàòûâàþòñÿ ïðèCheck(EX f , R) = CheckEX (Check(f , R))Check(E[fU,g ], R) = CheckEU(Check(f , R), Check(g , R)).îïèðàåòñÿ íà îïðåäåëåíèå òåìïîðàëüíîãîCheck(EG f , R) = CheckEG (Check(f , R))Ïðîöåäóðà CheckEXîïåðàòîðà :EX, ýòî OBDD, ïðåäñòàâëÿþùàÿ îòíîøåíèåCheckEX (f (v )) = ∃v 0 [f (v 0 ) ∧ R(v , v 0 )]ãäåïåðåõîäîâ.Ðàñïîëàãàÿ OBDD äëÿ f è R , ìîæíî âû÷èñëèòü OBDD äëÿR(v , v 0 ),∃v 0 [f (v 0 ) ∧ R(v , v 0 )]ïðè ïîìîùè îïåðàöèé íàä QBF.Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÏðîöåäóðà CheckEU îïèðàåòñÿ íà ôîðìóëó íàèìåíüøåéíåïîäâèæíîé òî÷êè, îïèñûâàþùóþ CTL îïåðàòîð :[f1 f2 ] = µZ .
f2 ∨ (f1 ∧Z) .Ïðè ïîìîùè ôóíêöèè âû÷èñëÿåòñÿ ïîñëåäîâàòåëüíîñòüQ0 , Q1 , Q2 , . . . , Qi , . . . ,ìíîæåñòâ ñîñòîÿíèé, ñõîäÿùàÿñÿ ê [f g ] çà êîíå÷ííîå ÷èñëîøàãîâ.Ðàñïîëàãàÿ ROBDD äëÿ f , g è òåêóùèì ïðèáëèæåíèåì Qi ,ìîæíî âû÷èñëèòü OBDD äëÿ ñëåäóþùåãî ïðèáëèæåíèÿ Qi+1 .Ïîñêîëüêó ROBDD ýòî êàíîíè÷åñêàÿ ôîðìà ïðåäñòàâëåíèÿáóëåâûõ ôóíêöèé, ñõîäèìîñòü ëåãêî ïðîâåðèòü, ñðàâíèâàÿïîñëåäîâàòåëüíûå ïðèáëèæåíèÿ. Êàê òîëüêî âûïîëíèòñÿðàâåíñòâî Qi = Qi+1 , ôóíêöèÿ ïðåêðàòèò âû÷èñëåíèÿ.Ìíîæåñòâî ñîñòîÿíèé, â êîòîðûõ âûïîëíÿåòñÿ [f g ] , áóäåòïðåäñòàâëåíî ROBDD äëÿ Qi .EUEUEXLfpEULfpEUÑèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÏðîöåäóðà CheckEG óñòðîåíà ñõîäíûì îáðàçîì.
 åå îñíîâåëåæèò ôîðìóëà íàèáîëüøåé íåïîäâèæíîé òî÷êè äëÿ CTLîïåðàòîðà :f1 = νZ . f1 ∧Z.Ðàñïîëàãàÿ OBDD äëÿ f1 , ìîæíî èñïîëüçîâàòü ôóíêöèþäëÿ âû÷èñëåíèÿ ROBDD, ïðåäñòàâëÿþùåé ìíîæåñòâîñîñòîÿíèé, â êîòîðûõ âûïîëíÿåòñÿ ôîðìóëà f1 .EGEGEXGfpEGÑèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÌåòîä ñèìâîëüíîé âåðèôèêàöèè ìîäåëåé ðàáîòàåò òàê.Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÌåòîä ñèìâîëüíîé âåðèôèêàöèè ìîäåëåé ðàáîòàåò òàê.1. äëÿ êàæäîãî îïåðàòîðà act âñÿêîãî ïðîöåññà Pïðîâåðÿåìîé ðàñïðåäåëåííîé ñèñòåìû Syst ñòðîèòñÿROBDD Ract , îïèñûâàþùàÿ îòíîøåíèå ïåðåõîäîâ íàìíîæåñòâå ñîñòîÿíèé âû÷èñëåíèÿ, êîòîðîå çàäàåòñÿ ýòèìîïåðàòîðîì.Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÌåòîä ñèìâîëüíîé âåðèôèêàöèè ìîäåëåé ðàáîòàåò òàê.1.
äëÿ êàæäîãî îïåðàòîðà act âñÿêîãî ïðîöåññà Pïðîâåðÿåìîé ðàñïðåäåëåííîé ñèñòåìû Syst ñòðîèòñÿROBDD Ract , îïèñûâàþùàÿ îòíîøåíèå ïåðåõîäîâ íàìíîæåñòâå ñîñòîÿíèé âû÷èñëåíèÿ, êîòîðîå çàäàåòñÿ ýòèìîïåðàòîðîì.2. äëÿ êàæäîãî ïðîöåññà P ïðîâåðÿåìîéSðàñïðåäåëåííîéñèñòåìû Syst ñòðîèòñÿ ROBDD RP = act∈P Ract ,îïèñûâàþùàÿ îòíîøåíèå ïåðåõîäîâ ýòîãî ïðîöåññà.Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÌåòîä ñèìâîëüíîé âåðèôèêàöèè ìîäåëåé ðàáîòàåò òàê.1. äëÿ êàæäîãî îïåðàòîðà act âñÿêîãî ïðîöåññà Pïðîâåðÿåìîé ðàñïðåäåëåííîé ñèñòåìû Syst ñòðîèòñÿROBDD Ract , îïèñûâàþùàÿ îòíîøåíèå ïåðåõîäîâ íàìíîæåñòâå ñîñòîÿíèé âû÷èñëåíèÿ, êîòîðîå çàäàåòñÿ ýòèìîïåðàòîðîì.2.
äëÿ êàæäîãî ïðîöåññà P ïðîâåðÿåìîéSðàñïðåäåëåííîéñèñòåìû Syst ñòðîèòñÿ ROBDD RP = act∈P Ract ,îïèñûâàþùàÿ îòíîøåíèå ïåðåõîäîâ ýòîãî ïðîöåññà.3. äëÿ ïðîâåðÿåìîé ðàñïðåäåëåííîé ñèñòåìû Syst âçàâèñèìîñòè îò âèäà ïàðàëëåëüíîé êîìïîçèöèè ñòðîèòñÿROBDD RSyst =kP∈Syst RP , îïèñûâàþùàÿ îòíîøåíèåïåðåõîäîâ ñèñòåìû.Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÌåòîä ñèìâîëüíîé âåðèôèêàöèè ìîäåëåé ðàáîòàåò òàê.1. äëÿ êàæäîãî îïåðàòîðà act âñÿêîãî ïðîöåññà Pïðîâåðÿåìîé ðàñïðåäåëåííîé ñèñòåìû Syst ñòðîèòñÿROBDD Ract , îïèñûâàþùàÿ îòíîøåíèå ïåðåõîäîâ íàìíîæåñòâå ñîñòîÿíèé âû÷èñëåíèÿ, êîòîðîå çàäàåòñÿ ýòèìîïåðàòîðîì.2. äëÿ êàæäîãî ïðîöåññà P ïðîâåðÿåìîéSðàñïðåäåëåííîéñèñòåìû Syst ñòðîèòñÿ ROBDD RP = act∈P Ract ,îïèñûâàþùàÿ îòíîøåíèå ïåðåõîäîâ ýòîãî ïðîöåññà.3.
äëÿ ïðîâåðÿåìîé ðàñïðåäåëåííîé ñèñòåìû Syst âçàâèñèìîñòè îò âèäà ïàðàëëåëüíîé êîìïîçèöèè ñòðîèòñÿROBDD RSyst =kP∈Syst RP , îïèñûâàþùàÿ îòíîøåíèåïåðåõîäîâ ñèñòåìû.4. ê ïîñòðîåííîé ROBDD RSyst è CTL ñïåöèôèêàöèè ϕïðèìåíÿåòñÿ ïðîöåäóðà Check(ϕ, RSyst ) è ïðîâåðÿåòñÿóñëîâèå S0 ⊆ Check(ϕ, RSyst ) .Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÌåòîä ñèìâîëüíîé âåðèôèêàöèè ìîäåëåé ðàáîòàåò òàê.1.
äëÿ êàæäîãî îïåðàòîðà act âñÿêîãî ïðîöåññà Pïðîâåðÿåìîé ðàñïðåäåëåííîé ñèñòåìû Syst ñòðîèòñÿROBDD Ract , îïèñûâàþùàÿ îòíîøåíèå ïåðåõîäîâ íàìíîæåñòâå ñîñòîÿíèé âû÷èñëåíèÿ, êîòîðîå çàäàåòñÿ ýòèìîïåðàòîðîì.2. äëÿ êàæäîãî ïðîöåññà P ïðîâåðÿåìîéSðàñïðåäåëåííîéñèñòåìû Syst ñòðîèòñÿ ROBDD RP = act∈P Ract ,îïèñûâàþùàÿ îòíîøåíèå ïåðåõîäîâ ýòîãî ïðîöåññà.3. äëÿ ïðîâåðÿåìîé ðàñïðåäåëåííîé ñèñòåìû Syst âçàâèñèìîñòè îò âèäà ïàðàëëåëüíîé êîìïîçèöèè ñòðîèòñÿROBDD RSyst =kP∈Syst RP , îïèñûâàþùàÿ îòíîøåíèåïåðåõîäîâ ñèñòåìû.4.
ê ïîñòðîåííîé ROBDD RSyst è CTL ñïåöèôèêàöèè ϕïðèìåíÿåòñÿ ïðîöåäóðà Check(ϕ, RSyst ) è ïðîâåðÿåòñÿóñëîâèå S0 ⊆ Check(ϕ, RSyst ) .Íà êàêîì ýòàïå âîçíèêàþò ñàìûå áîëüøèå òðóäíîñòè?Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÓïðàæíåíèå.Ïðèìåíèòå ïðîöåäóðû âû÷èñëåíèÿ íàèìåíüøåé íåïîäâèæíîéòî÷êè è íàèáîëüøåé íåïîäâèæíîé òî÷êè äëÿ ïðîâåðêèâûïîëíèìîñòè ôîðìóë CTL íà ìîäåëè è ïðîâåðüòå, â êàêèõñîñòîÿíèé s ñîáëþäàþòñÿ îòíîøåíèÿ âûïîëíèìîñòè M, s |= ϕäëÿ ïðèâåäåííûõ íèæå ôîðìóë íà ìîäåëè M ,LfpGfpI AF qI AG(AF(p∨ r ))I EX EX rI AG A[q Rp]Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÌîäåëü M s0 s q, r sp, q3kI@@@@6@@s1 ?r6&%@@ - p, t s2ÊÎÍÅÖ ËÅÊÖÈÈ 6..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
