Лекции В.А. Захарова, страница 35

Состояние вычисления программы π — этопара (состояние управления, состояние данных). Состояниеуправления — это значение счетчика команд программы.Состояние данных — это подстановка, указывающеясоответствие между переменными и их значениями.IЕсли в точке count1 программы π выполняется операторop, преобразующий данные из состояния ξ1 в состояние ξ2и передающий управление в точку count2 , то в LTSимеется переход (count1 , ξ1 ) −→ (count2 , ξ2 ).IАтомарным высказыванием p может быть любая формулалогики предикатов, зависящая от переменных программыи счетчика команд.

Разметка ρ определяется так:p ∈ ρ((count, ξ)) ⇐⇒ Iπ |= p[(count, ξ)].РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПрограмма драйвера π1while true doL1 : while R 6= free do wait od ;L2 : R = busy ;L3 : output(X,printer );L4 : R = free;odРАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS для программы π1t (L1 , {R/free})'- i t i(L1 , {R/busy })?i(L2 , {R/free}) ? i(L3 , {R/busy })&?i(L4 , {R/busy })РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыНекоторые переменные программы могут быть доступны длядругих программ (т. н. разделяемые переменные ) или дляокружающей среды (датчики, сенсоры, средства управления).В том случае, когда программа π взаимодействует сокружающей средой, в LTS Mπ вносятся следующиеизменения:для каждого состояния (l, ξ) вводятся переходы (l, ξ) −→ (l, ξ 0 )во всевозможные состояния (l, ξ 0 ), в которых подстановки ξ 0 ,отличающиеся от ξ только значениями переменных, доступныхдля окружающей среды.Например, полагая, что регистр принтера R — это тумблер,который может переключаться сколь угодно часто в разныемоменты времени, получим следующую LTS, описывающуювзаимодействие драйвера принтера с окружающей средой(пользователем принтера).РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS для системыπ1 k environment(L1 , {R/free})''-itI?iI'- ?i(L3 , {R/busy })I(L2 , {R/free})(L4 , {R/busy })&&?iI Rti (L1 , {R/busy })Ri(L2 , {R/busy })% R i (L , {R/free})3R?i%(L3 , {R/free})РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS для распределенной системы, состоящей из двух процессовπ1 и π2 , взаимодействующих посредством разделяемыхпеременных, строится на основе семантики чередующихсявычислений.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS для распределенной системы, состоящей из двух процессовπ1 и π2 , взаимодействующих посредством разделяемыхпеременных, строится на основе семантики чередующихсявычислений.Состояниями LTS для системы π1 k π2 объявляются наборы(count1 , count2 , ξ1 , ξ2 , χ), гдеIcount1 , count2 — значения счетчиков команд процессов π1и π2 ,Iξ1 , ξ2 — подстановки, определяющие значения локальныхпеременных процессов π1 и π2 ,Iχ — подстановка, определяющая значения разделяемыхпеременных.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS для распределенной системы, состоящей из двух процессовπ1 и π2 , взаимодействующих посредством разделяемыхпеременных, строится на основе семантики чередующихсявычислений.Переход (count1 , count2 , ξ1 , ξ2 , χ) −→ (count10 , count20 , ξ10 , ξ20 , χ0 )возможен в том и только том случае, когда выполнено одно издвух условий:Iв LTS M(π1 ) есть переход (count1 , ξ1 , χ) −→ (count10 , ξ10 , χ0 )и при этом count20 = count2 , ξ20 = ξ2 ;Iв LTS M(π2 ) есть переход (count2 , ξ2 , χ) −→ (count20 , ξ20 , χ0 )и при этом count10 = count1 , ξ10 = ξ1 .Таким образом, в семантике чередующихся вычисленийпараллельное выполнение процессов распределенной системымоделируется недетерминированным выбором того или иногопорядка, в котором выполняются действия разных процессов.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS для программы π 0- it (L01 , free)'и программы π 00 t (L001 , free)i 't- i(L01 , busy )(L001 , busy )?i(L02 , free)?i(L002 , free) ?i ?i (L03 , busy )? 0i(L4 , busy )& ti (L003 , busy )? 00i(L4 , busy )&РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS для системыπ10 k π100000- t(L1 , L1 , free)$'- i$@ (L01 , L002 , free)(L02 , L001 , free) tRt@ '$@66000R t@ (L2 , L2 , free)@ (L0 , L00 , busy )(L03 , L00, busy ) ? (L02 , L00(L01 , L00, busy ) ?13 , busy )332?R@-t ttt'$?@ R t(L03 , L003 , busy )@ I(L04 , L00(L01 , L001 , busy ) ?4 , busy )? t?t t?(L02 , L004 , busy )(L04 , L00, busy ) t&%2'000(L1 , L1 , busy )ti (L03 , L004 , busy ) ?(L04 , L00?3 , busy )t& - tH%YH*000L4 , busy ) H (L4 ,t H000000000, free) (L1 ,L4 , free)(L3 , L1 , free) ? (L4 , L1 H(L01 , L003 , free)H - t ?t - t- tHHHH,H(L02 , L00(L03 , L00, free) ? ?(L04, L00(L02 , L002 , free)4 free)23 , free)H?t ?- t- tt ЗАДАЧА ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММИтак, для верификации распределенных программ нужныIтребования правильности (спецификации) вычисленийпрограммы, представленные формулой PLTL ϕ,Iматематическая модель распределенной программы π,представленная конечной LTS M(π).Тогда для проверки правильности программы π достаточнопроверить, что для любой трассы tr , tr ∈ Tr0 (M(π)), формулаϕ выполняется в темпоральной интерпретации I (tr ), т.

е. имеетместо I (tr ), 0 |= ϕ.Воспользуемся записью M |= ϕ для обозначения утверждения«для любой трассы tr , tr ∈ Tr0 (M), имеет место I (tr ), 0 |= ϕ».ЗАДАЧА ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММЗадача верификации моделей программ (model checking) дляPLTL формулируется так:для заданной формулы PLTL ϕ и LTS M проверить M |= ϕ.Существует ли алгоритм решениязадачи верификации моделейпрограмм?КОНЕЦ ЛЕКЦИИ 21.Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. ÇàõàðîâËåêöèÿ 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), ò.