Лекция 22. Задача верификации моделей программ. Подформулы Фишера-Ладнера... (1161892)
Текст из файла
Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. ÇàõàðîâËåêöèÿ 22.Çàäà÷à âåðèôèêàöèè ìîäåëåéïðîãðàìì.Ïîäôîðìóëû Ôèøåðà-Ëàäíåðà.Òàáëè÷íûé ìåòîä âåðèôèêàöèèìîäåëåé ïðîãðàìì.Àëãîðèòì âåðèôèêàöèè ìîäåëåéïðîãðàìì.ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÇàäà÷à model checking äëÿ PLTLÄëÿ çàäàííîé ôîðìóëû PLTL ϕ è êîíå÷íîé LTS M ïðîâåðèòü M |= ϕ.Ïî÷åìó çàäà÷à model checking íåïðîñòà? Ïîòîìó ÷òîIâûïîëíèìîñòü ôîðìóë PLTL ïðîâåðÿåòñÿ íà áåñêîíå÷íûõèíòåðïðåòàöèÿõ,I LTS M èìååòñÿ áåñêîíå÷íî ìíîãî èíòåðïðåòàöèé (òðàññ).Ïî÷åìó çàäà÷à model checking èìååò ýôôåêòèâíîå ðåøåíèå?Ïîòîìó ÷òîIâñå ýòî áåñêîíå÷íîå ìíîæåñòâî áåñêîíå÷íûõ èíòåðïðåòàöèé¾óïàêîâàíî¿ â êîíå÷íóþ ñòðóêòóðó LTS M .ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÇàìûñåë òàáëè÷íîãî ìåòîäà1.
Âìåñòî ïðîâåðêè âûïîëíèìîñòè ϕ âî âñåõ èíòåðïðåòàöèÿõëó÷øå çàíÿòüñÿ ïîèñêîì êîíòðìîäåëè èíòåðïðåòàöèè I ,â êîòîðîé íå âûïîëíÿåòñÿ ϕ.2. Âûïîëíèìîñòü âñÿêîé ôîðìóëû ψ ïîëíîñòüþ îïðåäåëÿåòñÿâûïîëíèìîñòüþ åå ïîäôîðìóë. Ïîýòîìó (íå)âûïîëíèìîñòüôîðìóë ìîæíî ïðîâåðÿòü èíäóêòèâíî.3. (Íå)âûïîëíèìîñòü ôîðìóëû íà îäíîé èç òðàññ LTS M ,íà÷èíàþùåéñÿ â ñîñòîÿíèè s , ýòî ñâîéñòâî ñîñòîÿíèÿ s .Çíà÷èò, ïðîâåðÿÿ (íå)âûïîëíèìîñòü âñåõ ïîäôîðìóëôîðìóëû ϕ äëÿ âñåõ ñîñòîÿíèé LTS M , ìîæíî âû÷èñëèòüìíîæåñòâî S ϕ âñåõ òåõ ñîñòîÿíèé, â êîòîðûõ íåâûïîëíÿåòñÿ ôîðìóëà ϕ. Åñëè S0 ∩ S ϕ 6= ∅, òî M 6|= ϕ.ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÂñïîìîãàòåëüíûå îïðåäåëåíèÿ è îáîçíà÷åíèÿÄëÿ çàäàííîé LTS M = hAP, S, S0 , −→, ρi, òðàññûtr = si0 , si1 , .
. . , sin , sin+1 , . . . â LTS M è ôîðìóëû PLTL ϕ áóäåìèñïîëüçîâàòü çàïèñüItr |= ϕ äëÿ îáîçíà÷åíèÿ îòíîøåíèÿ âûïîëíèìîñòèI (tr ), 0 |= ϕ;Itr [j] äëÿ îáîçíà÷åíèÿ j -ãî ñîñòîÿíèÿ sij â òðàññå tr ;Itr |j äëÿ îáîçíà÷åíèÿ òðàññû tr 0 = sij , sij+1 , . . . , ÿâëÿþùåéñÿñóôôèêñîì òðàññû tr , íà÷èíàþùåéñÿ ñîñòîÿíèåì sij .ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÓòâåðæäåíèå 1.Äëÿ ëþáîé LTS M è ôîðìóëà PLTL ϕ âåðíîM 6|= ϕ⇐⇒ñóùåñòâóåò òàêàÿ íà÷àëüíàÿ òðàññà tr , tr ∈ Tr0 (M),äëÿ êîòîðîé tr 6|= ϕ.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.Òàêèì îáðàçîì, âìåñòî çàäà÷è M |= ϕ ìû áóäåì ðàññìàòðèâàòüäðóãóþ çàäà÷ó:íàéòè â LTS M íà÷àëüíóþ òðàññó tr , äëÿ êîòîðîé tr 6|= ϕ.Åñëè òàêîé òðàññû íàéòè íå óäàñòñÿ, òî âåðíî M |= ϕ.ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÏðèâåäåíèå ôîðìóëû ê ïîçèòèâíîé ôîðìåÏðèìåíÿÿ ðàâíîñèëüíûå ïðåîáðàçîâàíèÿ, óïðîñòèì ôîðìóëó ϕ.Óäàëåíèå èìïëèêàöèè → è òåìïîðàëüíûõ îïåðàòîðîâíà îñíîâàíèè çàêîíîâ âçàèìíîé çàâèñèìîñòèÝòàï 1.,G F|= ψ → ψ ≡ ¬ψ ∨ χ;|= Fψ ≡ true Uψ ;|= Gψ ≡ false Rψ .Ýòàï 2.
Ïðîäâèæåíèå ¬ âãëóáü ôîðìóëû íà îñíîâàíèè çàêîíîâäâîéñòâåííîñòè|= ¬(ψ&χ) ≡ ¬ψ ∨ ¬χ;|= ¬(ψ ∨ χ) ≡ ¬ψ&¬χ;|= ¬¬ψ ≡ ψ ;|= ¬Xψ ≡ X¬ψ ;|= ¬(ψUχ) ≡ ¬ψR¬χ;|= ¬(ψRχ) ≡ ¬ψU¬χ.ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÓòâåðæäåíèå 2. ðåçóëüòàòå ïðèìåíåíèÿ ðàâíîñèëüíûõ ïðåîáðàçîâàíèé ýòàïîâ1 è 2 ëþáàÿ ôîðìóëà PLTL ϕ ïðèâîäèòñÿ ê ðàâíîñèëüíîéôîðìóëå ϕ0 , ïðåäñòàâëåííîé â ïîçèòèâíîé ôîðìå, â êîòîðîéIèñïîëüçóþòñÿ òîëüêî ëîãè÷åñêèå ñâÿçêè ∨, &, ¬ èòåìïîðàëüíûå îïåðàòîðû X, F, G,Iñâÿçêà ¬ ïðèìåíÿåòñÿ òîëüêî ê àòîìàðíûì âûñêàçûâàíèÿìp, p ∈ AP .Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.ÇÀÄÀ×À ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÏðèâåäåíèå ôîðìóëû ê ïîçèòèâíîé ôîðìåÏðèìåð.ϕ = G(free & Xbusy → XF(pr1 ∨ pr2 )).Ýòàï 1.ϕ0 = false R (¬(free & Xbusy ) ∨ X(true U(pr1 ∨ pr2 ))).Ýòàï 2.ϕ1 = false R (¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 ))).ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÏóñòü ϕ1 ôîðìóëà PLTL â ïîçèòèâíîé ôîðìå.
Òîãäàìíîæåñòâîì ïîäôîðìóë ÔèøåðàËàäíåðà íàçûâàåòñÿíàèìåíüøåå ìíîæåñòâî ôîðìóë PLTL FLSubϕ1 , ñîäåðæàùååôîðìóëó ϕ1 è óäîâëåòâîðÿþùåå ñëåäóþùèì óñëîâèÿì:Iåñëè p ∈ FLSubϕ1 è p ∈ AP , òî ¬p ∈ FLSubϕ1 ,Iåñëè ψ&χ ∈ FLSubϕ1 , òî {ψ, χ} ⊆ FLSubϕ1 ,Iåñëè ψ ∨ χ ∈ FLSubϕ1 , òî {ψ, χ} ⊆ FLSubϕ1 ,Iåñëè ¬ψ ∈ FLSubϕ1 , òî ψ ∈ FLSubϕ1 ,IåñëèIåñëè ψ Uχ ∈ FLSubϕ1 , òî {ψ, χ, X(ψ Uχ)} ⊆ FLSubϕ1 ,Iåñëè ψ Rχ ∈ FLSubϕ1 , òî {ψ, χ, X(ψ Rχ)} ⊆ FLSubϕ1 .Xψ ∈ FLSubϕ1 , òî ψ ∈ FLSubϕ1 ,Óòâåðæäåíèå 3.Åñëè ϕ1 ñîäåðæèò n ëîãè÷åñêèõ ñâÿçîê è òåìïîðàëüíûõîïåðàòîðîâ, òî |FLSubϕ1 | ≤ 3n.ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÏðèìåð.Ïóñòüϕ1 = false R (¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 ))).ÒîãäàFLSubϕ1= {ϕ1 ,false, Xϕ1 , ¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 )),¬free, X¬busy , X(true U(pr1 ∨ pr2 )),free, ¬busy , true U(pr1 ∨ pr2 ),busy , true, pr1 ∨ pr2 ,pr1 , pr2 , ¬pr1 , ¬pr2 }.ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀNext-ïîäôîðìóëûÏóñòü ϕ1 ôîðìóëà PLTL â ïîçèòèâíîé ôîðìå è FLSubϕ1 ìíîæåñòâîì ïîäôîðìóë ÔèøåðàËàäíåðà ôîðìóëû ϕ1 .Òîãäà çàïèñü XSubϕ1 áóäåò îáîçíà÷àòü ìíîæåñòâî âñåõ òåõïîäôîðìóë ÔèøåðàËàäíåðà, êîòîðûå íà÷èíàþòñÿ îïåðàòîðîìX (neXttime), ò.
å.XSubϕ1 = {ψ : ψ = Xχ, ψ ∈ FLSubϕ1 }.Ïðèìåð.Ïóñòüϕ1 = false R (¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 ))).ÒîãäàXSubϕ1= {Xϕ1 , X¬busy ,X(true U(pr1 ∨ pr2 ))}.ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀ(Until-Release)-ïîäôîðìóëûÏóñòü ϕ1 ôîðìóëà PLTL â ïîçèòèâíîé ôîðìå è FLSubϕ1 ìíîæåñòâîì ïîäôîðìóë ÔèøåðàËàäíåðà ôîðìóëû ϕ1 .Òîãäà çàïèñü URSubϕ1 áóäåò îáîçíà÷àòü ìíîæåñòâî âñåõ òåõïîäôîðìóë ÔèøåðàËàäíåðà, êîòîðûå íà÷èíàþòñÿ îïåðàòîðîìU (Until) èëè R (Release), ò. å.USubϕ1= {ψ : ψ = χ1 Uχ2 , ψ ∈ FLSubϕ1 }∪{ψ : ψ = χ1 Rχ2 , ψ ∈ FLSubϕ1 }.Ïðèìåð.Ïóñòüϕ1 = false R (¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 ))).ÒîãäàUSubϕ1= {ϕ1 , true U(pr1 ∨ pr2 )}.ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÑîãëàñîâàííûå ìíîæåñòâà ïîäôîðìóëÏóñòü ϕ1 ôîðìóëà PLTL â ïîçèòèâíîé ôîðìå, è FLSubϕ1 ìíîæåñòâî ïîäôîðìóë ÔèøåðàËàäíåðà äëÿ ϕ1 .Òîãäà ñîãëàñîâàííûì ìíîæåñòâîì ïîäôîðìóë ôîðìóëû ϕ1íàçûâàåòñÿ âñÿêîå ïîäìíîæåñòâî B , B ⊆ FLSubϕ1 ,óäîâëåòâîðÿþùåå ñëåäóþùèì óñëîâèÿì:1.true∈ B,false∈/ B,2.
äëÿ ëþáîãî àòîìàðíîãî âûñêàçûâàíèÿp, p ∈ AP ∩ FLSubϕ1 , âûïîëíÿåòñÿ â òî÷íîñòèäâóõ âêëþ÷åíèé: ëèáî p ∈ B , ëèáî ¬p ∈ B ;îäíî èç3. ψ ∨ χ ∈ B ⇐⇒ ψ ∈ B èëè χ ∈ B ,4. ψ&χ ∈ B ⇐⇒ ψ ∈ B è χ ∈ B ,5. ψ Uχ ∈ B ⇐⇒ χ ∈ B èëè {ψ, X(ψ Uχ)} ⊆ B ,6. ψ Rχ ∈ B ⇐⇒ χ ∈ B è ïðè ýòîì ψ ∈ B èëè X(ψ Rχ) ∈ B .ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÑîãëàñîâàííûå ìíîæåñòâà ïîäôîðìóëÑîãëàñîâàííûå ìíîæåñòâà ïîäôîðìóë ýòî ìàêñèìàëüíûåìíîæåñòâà ôîðìóë, êîòîðûå íå ñîäåðæàò ¾ÿâíûõ¿ïðîòèâîðå÷èé, ò.
å. òàêèõ ïðîòèâîðå÷èé, êîòîðûå ìîæíîîáíàðóæèòü â òåêóùèé ìîìåíò âðåìåíè.Íàïðèìåð, ìíîæåñòâî, ñîñòîÿùåå èç äâóõ ôîðìóëXpX¬p çàâòðà ÿ ïîéäó íà ëåêöèþ, çàâòðà ÿ íå ïîéäó íà ëåêöèþ,ìîæåò áûòü ñîãëàñîâàííûì (õîòÿ è ïðîòèâîðå÷èâûì),ïîñêîëüêó ñåãîäíÿ âîçìîæíîå ïðîòèâîðå÷èå, ñîäåðæàùååñÿ âýòèõ âûñêàçûâàíèÿõ, íå ïðîÿâëÿåòñÿ.Ñîãëàñîâàííîå ìíîæåñòâî ïîäôîðìóë ÿâëÿåòñÿ àíàëîãîìñåìàíòè÷åñêîé òàáëèöû îíî âûðàæàåò íàøå ïîæåëàíèåñäåëàòü âñå óòâåðæäåíèÿ, ñîäåðæàùèåñÿ â ýòîì ìíîæåñòâå,èñòèííûìè, à âñå óòâåðæäåíèÿ, íå ñîäåðæàùèåñÿ â íåì, ëîæíûìè.ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÑîãëàñîâàííûå ìíîæåñòâà ïîäôîðìóëÏðèìåð.ÏóñòüFLSubϕ1= {free, busy , pr1 , pr2 , ¬free, ¬busy , ¬pr1 , ¬pr2 ,pr1 ∨ pr2 ,true U(pr1 ∨ pr2 ),X¬busy , X(true U(pr1 ∨ pr2 )),¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 )),ϕ1 , Xϕ1 }.Òîãäà îäíèì èç ñîãëàñîâàííûõ ìíîæåñòâ ïîäôîðìóë ôîðìóëûϕ1 ÿâëÿåòñÿ ìíîæåñòâîB = {true, pr1 , ¬pr2 , ¬free, busy , X¬busy ,true U(pr1 ∨ pr2 ), X(true U(pr1 ∨ pr2 )), ϕ1 }.ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÓòâåðæäåíèå 4.Ïóñòü I ïðîèçâîëüíàÿ òåìïîðàëüíàÿ èíòåðïðåòàöèÿ, è ϕ1 ïðîèçâîëüíàÿ ôîðìóëà â ïîçèòèâíîé ôîðìå.Òîãäà äëÿ ëþáîãî ìîìåíòà âðåìåíè n ìíîæåñòâî ôîðìóëBn = {ψ : ψ ∈ FLSubϕ1 è I , n |= ψ}ÿâëÿåòñÿ ñîãëàñîâàííûì.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.
Íåïîñðåäñòâåííî èç îïðåäåëåíèÿñîãëàñîâàííîãî ìíîæåñòâà.À âåðíî ëè îáðàòíîå óòâåðæäåíèå: êàæäîå ñîãëàñîâàííîåìíîæåñòâî ôîðìóë âûïîëíèìî â íåêîòîðîé èíòåðïðåòàöèè âíà÷àëüíûé ìîìåíò âðåìåíè?ÏÎÄÔÎÐÌÓËÛ ÔÈØÅÐÀËÀÄÍÅÐÀÓòâåðæäåíèå 5.Ïóñòü ϕ1 ôîðìóëà PLTL â ïîçèòèâíîé ôîðìå. Òîãäà1. äëÿ ëþáîé ïàðû B 0 ⊆ AP ∩ FLSubϕ1 , B 00 ⊆ XSubϕ1 ,ñóùåñòâóåò òàêîå ñîãëàñîâàííîå ìíîæåñòâî ïîäôîðìóë B ,äëÿ êîòîðîãî âåðíî B ∩ AP = B 0 , B ∩ XSubϕ1 = B 00 ;2.
äëÿ ëþáîé ïàðû B1 è B2 ñîãëàñîâàííûõ ìíîæåñòâïîäôîðìóë Ôèøåðà-Ëàäíåðà ϕ1 âåðíû ñîîòíîøåíèÿB1 = B2 ⇐⇒ B1 ∩ AP = B2 ∩ AP èB1 ∩ XSubϕ1 = B1 ∩ XSubϕ1 .Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.Óòâåðæäåíèå 6.Åñëè ϕ1 ñîäåðæèò n ëîãè÷åñêèõ ñâÿçîê è òåìïîðàëüíûõîïåðàòîðîâ, òî ÷èñëî ðàçëè÷íûõ ñîãëàñîâàííûõ ìíîæåñòâïîäôîðìóë Ôèøåðà-Ëàäíåðà íå ïðåâîñõîäèò âåëè÷èíû 23n .ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÌÎÄÅËÅÉ ÏÐÎÃÐÀÌÌÏóñòü çàäàíà ôîðìóëû PLTL ϕ è êîíå÷íàÿ LTSM = hAP, S, S0 , −→, ρi.Íóæíî ïðîâåðèòü âûïîëíèìîñòü M |= ϕ.Äëÿ ýòîãî1. ôîðìóëà ϕ ïðèâîäèòñÿ ê ïîçèòèâíîé ôîðìå ϕ1 ,2.
äëÿ ôîðìóëû ϕ1 ñòðîÿòñÿIIIIìíîæåñòâî ïîäôîðìóë ÔèøåðàËàäíåðà FLSubϕ1 ,ìíîæåñòâî Next-ïîäôîðìóë XSubϕ1 ,ìíîæåñòâî U-ïîäôîðìóë FLSubϕ1 ,ñîâîêóïíîñòü Conϕ1 âñåõ âîçìîæíûõ ñîãëàñîâàííûõìíîæåñòâ ïîäôîðìóë ÔèøåðàËàäíåðà.ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÌÎÄÅËÅÉ ÏÐÎÃÐÀÌÌÑèñòåìîé Õèíòèêêè äëÿ ôîðìóëû PLTL ϕ1 è LTS Míàçûâàåòñÿ ðàñêðàøåííûé îðèåíòèðîâàííûé ãðàôGϕ1 ,M = (V , E ) ñ ìíîæåñòâîì âåðøèí V è ìíîæåñòâîì äóã E ,êîòîðûå óñòðîåíû òàê:V = {(s, B) : s ∈ S, B ∈ Conϕ1 , ρ(s) = B ∩ AP},ò. å. âåðøèíàìè ãðàôà ÿâëÿþòñÿ âñåâîçìîæíûå ïàðû(ñîñòîÿíèå s , ñîãëàñîâàííîå ìíîæåñòâî B ),äëÿ êîòîðûõ ðàçìåòêà ρ(s) ñîñòîÿíèÿ s ïîäòâåðæäàåòèñòèííîñòü âñåõ àòîìàðíûõ âûñêàçûâàíèé ìíîæåñòâà B ;E= {h(s 0 , B 0 ), (s 00 , B 00 )i : s 0 −→ s 00è äëÿ ëþáîé Next-ïîäôîðìóëûâåðíî Xψ ∈ B 0 ⇐⇒ ψ ∈ B 00 },Xψ, Xψ ∈ XSubϕ1 ,ò.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
