Лекция 21. Верификация распределенных программ. Логика линейного времени PLTL... (Лекции 2014), страница 2

Следует непосредственно из определенияотношения выполнимости.Покажем справедливость соотношения 4).ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLДоказательство.Пусть I , 0 |= ¬(ϕUψ), т. е. I , 0 6|= ϕUψ. Тогда согласноопределению отношения выполнимости для оператора U вернохотя бы одно из двух:1.

либо для любого k, k ≥ 0, верно I , k 6|= ψI , 0 6|= ψ- y0I , 1 6|= ψ- y- y12- yI , k 6|= ψ- y-r r rk2. либо существует такое k, k ≥ 0, что I , k 6|= ψ, I , k 6|= ϕи при этом для любого i если 0 ≤ i < k, то I , k 6|= ψ, I , k |= ϕr r rI , 0 6|= ψI , 0 |= ϕ- y0I , 1 6|= ψI , 1 |= ϕ- y1I,k −1 6|= ψI,k −1 |= ϕ- y2- yI,k 6|= ψI,k 6|= ϕ- yk-r r rЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLДоказательство.Но это означает, что верно хотя бы одно из двух:1. либо для любого k, k ≥ 0, верно I , k |= ¬ψI , 0 |= ¬ψ I , 1 |= ¬ψ- y- y- y012- yI , k |= ¬ψ- y-r r rk2.

либо существует такое k, k ≥ 0, что I , k |= ¬ψ, I , k |= ¬ϕи при этом для любого i если 0 ≤ i < k, то I , k |= ¬ψI , 0 |= ¬ψ I , 1 |= ¬ψr r r- y0- y1I,k −1 |= ¬ψ- y2- yI,k |= ¬ψI,k |= ¬ϕ- y-n+kА это как раз и означает, что I , 0 |= (¬ϕ)R(¬ψ).Значит, I |= ¬(ϕUψ) → ¬ϕR¬ψ для любой интерпретации I .r r rЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLДоказательство.Проводя аналогичные рассуждения покажите самостоятельно ,что верно соотношениеI |= ¬ϕR¬ψ → ¬(ϕUψ),а также остальные законы двойственности темпоральныхоператоров.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLРавносильные формулыЗаконы взаимной зависимости.1.

|= Fϕ ≡ ¬G¬ϕ;2. |= Gϕ ≡ ¬F¬ϕ;3. |= ϕUψ ≡ ¬(¬ϕR¬ψ);4. |= ϕRψ ≡ ¬(¬ϕU¬ψ);5. |= Fϕ ≡ true Uϕ;6. |= Gϕ ≡ false Rϕ.Доказательство. Самостоятельно.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLРавносильные формулыЗаконы неподвижной точки.1. |= Fϕ ≡ ϕ ∨ XFϕ;2. |= Gϕ ≡ ϕ & XGϕ;3. |= ϕUψ ≡ ψ ∨ (ϕ & X(ϕUψ);4. |= ϕRψ ≡ ψ & (ϕ ∨ X(ϕRψ).Доказательство. Самостоятельно.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLРавносильные формулыА какие законы дистрибутивности верны?1. |= F(ϕ ∨ ψ) ≡???;2. |= G(ϕ ∨ ψ) ≡???;3. |= F(ϕ&ψ) ≡???;4. |= G(ϕ&ψ) ≡???;5.

|= ϕU(ψ ∨ χ) ≡???;6. |= ϕU(ψ&χ) ≡???7. |= (ϕ ∨ χ)Uχ ≡???;8. |= (ϕ&χ)Uχ ≡???.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLВыразительные возможности PLTLА теперь посмотрим, насколько адекватно и просто можновыражать при помощи PLTL те требования, которыепредъявляются к поведению распределенных систем программ.1. Всякий раз, когда принтер свободен и хотя бы одинкомпьютер собирается отправить данные на печать,принтер будет рано или поздно занят;2. Всякий раз, после того как принтер оказался занят, ондолжен когда-нибудь приступить к печати;3. Компьютер, завершивший печать, должен когда-нибудьосвободить принтер;4. Данные на печать всегда передает не более чем одинкомпьютер.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLВыразительные возможности PLTLВведем следующие атомарные высказывания, соответствующиеосновным событиям вычислений программы:1.

tryi — i-ый компьютер собирается отправить данные напечать;2. pri — i-ый компьютер передает данные на печать;3. free — принтер свободен;4. busy — принтер занят.Пусть имеется система, состоящая из 2 компьютеров.Тогда все перечисленные требования выражаются формуламиPLTL так.ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLВыразительные возможности PLTL1. Всякий раз, когда принтер свободен и хотя бы одинкомпьютер собирается отправить данные на печать,принтер будет рано или поздно занят:ϕ1 = G((free & (try1 ∨ try2 )) → Fbusy ) ;2. Всякий раз, после того как принтер оказался занят, ондолжен когда-нибудь приступить к печати:ϕ2 = G(free & Xbusy → XF(pr1 ∨ pr2 )) ;ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLВыразительные возможности PLTL3.

Компьютер, завершивший печать, должен когда-нибудьосвободить принтер:ϕ3i = G(pri & X¬pri → XFfree) ;4. Данные на печать всегда передает не более чем одинкомпьютер:ϕ4 = G(¬(pr1 & pr2 )) .ЛОГИКА ЛИНЕЙНОГО ВРЕМЕНИ PLTLВыразительные возможности PLTL5. До тех пор пока хотя бы один компьютер отправляетданные на печать, принтер остается занятым:ϕ5 = G((¬(pr1 ∨ pr2 ) R busy ) ;или может быть это лучше выразить так:ϕ05 = G(busy R (¬(pr1 ∨ pr2 ))) ?или может быть так:ϕ005 = G((pr1 ∨ pr2 ) → busy ) ?РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВТеперь мы можем использовать PLTL в качестве формальногоязыка спецификации программ.Чтобы иметь возможность проверить, удовлетворяют ли всевычисления распределенной системы программ заданнымспецификациям, которые представлены формулами PLTL,нужно определить математическую модель программ.При разработке математической модели программ нужностремиться к тому, чтобыIкаждое вычисление распределенной системы программпредставляло собой темпоральную интерпретацию;Iвычисления программ в предложенной математическоймодели соответствовали реальному поведениювычислительных устройств, выполняющих эти программы;Iмодель программ имела простое устройство.В качестве такой модели программ мы будем использоватьразмеченные системы переходов .РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВОпределение LTSРазмеченная система переходов (LTS, Labelled TransitionSystem) — это пятерка hAP, S, S0 , −→, ρi, в которой1.

AP — множество атомарных высказываний;2. S — непустое множество состояний вычислений;3. S0 , S0 ⊆ S, — непустое подмножество начальныхсостояний;4. −→⊆ S × S, — тотальное отношение переходов,тотальность отношения −→ означает, что для любогосостояния s, s ∈ S, существует такое состояние s 0 , чтоs −→ s 0 (т. е.

из любого состояния можно сделать хотя быодин переход);5. ρ : S → 2AP — функция разметки, приписывающаякаждому состоянию вычислений s, s ∈ S, множествоρ(s), ρ(s) ⊆ AP, всех тех атомарных высказываний,которые являются истинными в состоянии s.РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSM = hAP, S, S0 , T , ρiAP = {p, q},S = {s1 , s2 , s3 , s4 , s5 , s6 , s7 },'s1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- yS0 = {s1 , s2 }@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и PLTL-интерпретацииТрассой в LTS M = hAP, S, S0 , −→, ρi называется всякаябесконечная последовательность состоянийtr = si0 , si1 , .

. . , sin , sin+1 , . . . ,(∗)в которой для любого n, n > 0, верно (sin −→ sin+1 ).Если si0 — начальное состояние, si0 ∈ S0 , то трасса trназывается начальной трассой.Запись Tr (M) обозначает множество всех трасс LTS M, азапись Tr0 (M) — множество всех начальных трасс LTS M.Каждой трассе tr ∈ Tr (M) вида (∗) сопоставимPLTL-интерпретацию I (tr ) = hN, ≤, ξi, в которой для любогоn, n ≥ 0, и p, p ∈ AP, верно соотношениеξ(n, p) = true ⇐⇒ p ∈ ρ(sin ) .РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falsey0s2's1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- y@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = true- y0s21s4's1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- y@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = truep = falseq = false- y- y1s42s30s2's1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- y@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = truep = falseq = falsep = falseq = true- y- y- y1s42s33s50s2's1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- y@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВПример LTSp = trueq = falseyp = truep = truep = falseq = falsep = falseq = true- y- y- y1s42s33s50s2-'s1 , {p, q}yI@@s3 , ∅- y6s5 , {q}- yr r r@@@ys2 , {p}@@@ys4 , {p, q}?ys6 , {p, q}?- y%s7 , {p}РАЗМЕЧЕННЫЕ СИСТЕМЫ ПЕРЕХОДОВLTS и распределенные программыLTS, соответствующую программе π, можно построить так:IСостояниями LTS полагаются состояния вычисленияпрограммы.

Состояние вычисления программы π — этопара (состояние управления, состояние данных). Состояниеуправления — это значение счетчика команд программы.Состояние данных — это подстановка, указывающеясоответствие между переменными и их значениями.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..