LectLog22 (1158012), страница 2
Текст из файла (страница 2)
, χ0k Uχ00k , χ0k+1 Rχ00k+1 , . . . , χ0k+m Rχ00k+m }.Каждой формуле ψi из множества URSubϕ1 сопоставиминдивидуальный цвет i.Раскрасим в цвет i все вершины (s, B), для которых выполненохотя бы одно из двух условийв случае, когда ψi = χ0i Uχ00i :1) χ00i ∈ B,2) X(χ0i Uχ00i ) ∈/ B.в случае, когда ψi = χ0i Rχ00i :/ B,1) χ00i ∈2) X(χ0i Rχ00i ) ∈ B.Бесконечный маршрут(si1 , Bi1 ), (si2 , Bi2 ), . . .
, (sin , Bin ), . . .в графе Γϕ1 ,M назовем радужным, если в нем бесконечно частовстречаются вершины каждого цвета 1, 2, . . . , k.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИОсновная теоремаДля любой формулы PLTL ϕ1 в позитивной форме и LTSM = hAP, S, S0 , −→, ρiM 6|= ϕ1mв графе Γϕ1 ,M существует хотя бы один радужный маршрут,исходящий из вершины v0 = (s0 , B0 ), в которой s0 ∈ S0 иϕ1 ∈/ B0 .ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДоказательство.(⇑) Предположим, что в графе Γϕ1 ,M есть радужный маршрут(s0 , B0 ), (s1 , B1 ), . .
. , (sn , Bn ), (sn+1 , Bn+1 ), . . .указанного вида, в котором ϕ1 ∈/ B0 .Тогда согласно определению системы Хинтикки Γϕ1 ,M в LTS Mесть начальная трассаtr |0 |= B0tr = ys0tr |1 |= B1tr |2 |= B2- y- ys1s2- r r rtr |n |= Bn- ysntr |n+1 |= Bn+1- y- r r rsn+1Покажем, что для любой формулы ψ, ψ ∈ FLSubϕ1 , и длялюбого n, n ≥ 0, верноtr |n |= ψ ⇐⇒ ψ ∈ Bn .ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДоказательство.Если удастся показать, чтоtr |n |= ψ ⇐⇒ ψ ∈ Bn(∗)то, учитывая ϕ1 ∈/ B0 , придем к заключению tr 6|= ϕ1 .Для доказательства соотношения (∗) воспользуемся индукциейпо числу связок в формуле ψ.Базис индукции.
p ∈ AP.p ∈ Bn ⇐⇒ p ∈ ξ(sn ) ⇐⇒ tr |n |= p .¬p ∈ Bn ⇐⇒ p ∈/ Bn ⇐⇒ p ∈/ ξ(sn ) ⇐⇒ tr |n 6|= p ⇐⇒ tr |n |= ¬p.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДоказательство.Индуктивный переход.1. Логические связки & и ∨.ψ1 &ψ2 ∈ Bn ⇐⇒ ψ1 ∈ Bn и ψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 и tr |n |= ψ1⇐⇒ tr |n |= ψ1 &ψ1 .2.
Темпоральный оператор X.Xψ ∈ Bn ⇐⇒ ψ ∈ Bn+1 ⇐⇒ tr |n+1 |= ψ ∈ Bn+1 ⇐⇒ tr |n |= Xψ.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.3. Темпоральный оператор R.3.1. Покажем ψ1 Rψ2 ∈ Bn =⇒ tr |n |= ψ1 Rψ2 .Заметим, что согласно определению согласованного множестваψ1 Rψ2 ∈ B ⇐⇒ ψ2 ∈ B и при этом ψ1 ∈ B или X(ψ1 Rψ2 ) ∈ B.Пусть ψ1 Rψ2 ∈ Bn . Тогда возможны 2 случая.Вариант 1. X(ψ1 Rψ2 ) ∈ Bn+i для любого i, i ≥ 0.Тогда по определению Γϕ1 ,M в каждом множестве Bn+i , i ≥ 0,содержится формула ψ1 Rψ2 и, следовательно, ψ2 ∈ Bn+i .Тогда по индуктивному предположению tr |n+i |= ψ2 для любогоi, i ≥ 0.
Следовательно, tr |n |= ψ1 Rψ2 .rrrtr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1- yn+2- ytr |n+i |= ψ2- yn+i-r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.Вариант 2. X(ψ1 Rψ2 ) ∈/ Bn+k для некоторого k, k ≥ 0.Тогда существует такое k0 , что X(ψ1 Rψ2 ) ∈/ Bn+k0 ноX(ψ1 Rψ2 ) ∈ Bn+i для любого i, 0 ≤ i < k0 .Тогда по определению графа Γϕ1 ,M в каждом множестве Bn+i ,0 ≤ i ≤ k0 , содержится формула ψ1 Rψ2 .Тогда по определению согласованных множеств ψ2 ∈ Bn+i длялюбого i, 0 ≤ i ≤ k0 , и, кроме того, ψ1 ∈ Bn+k0 .Тогда по индуктивному предположению tr |n+i |= ψ2 для любого0 ≤ i ≤ k0 и tr |n+k0 |= ψ1 .
Значит, tr |n |= ψ1 Rψ2 .rrrtr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1tr |n+k0 −1 |= ψ2- yn+2- ytr |n+k0 |= ψ1tr |n+k0 |= ψ2- y-n+kИтак, в обоих случаях ψ1 Rψ2 ∈ Bn =⇒ tr |n |= ψ1 Rψ2 .r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.3.2. Покажем ψ1 Rψ2 ∈/ Bn =⇒ tr |n 6|= ψ1 Rψ2 .Пусть ψ1 Rψ2 ∈/ Bn . Т. к. ψ1 Rψ2 ∈ URSubϕ1 этой формулесоответствует некоторый цвет j.Поскольку рассматриваемый маршрут(s0 , B0 ), (s1 , B1 ), . . . , (sn , Bn ), (sn+1 , Bn+1 ), .
. .является радужным, то вершины, окрашенные в цвет j,встречаются в этом маршруте бесконечно часто.Значит, существует такое k, k ≥ 0, что вершина (sn+k , Bn+k ) —первая, окрашенная в цвет j вершина, следующая в этомрадужном маршруте вслед за вершиной (sn , Bn ).Имеются две причины, по которым вершина (sn+k , Bn+k )оказалась окрашенной в цвет j:I ψ2 ∈/ Bn+k ,I X(ψ1 Rψ2 ) ∈ Bn+k ,Рассмотрим каждый из этих случаев по отдельности.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.Вариант 1.
ψ2 ∈/ Bn+k .Т. к. все вершины (sn+i , Bn+i ), 0 ≤ i < k не окрашены в цвет j,для каждого из множеств Bn+i , 0 ≤ i < k, верны соотношенияψ2 ∈ Bn+iиX(ψ1 Rψ2 ) ∈/ Bn+i .Тогда по определению графа Γϕ1 ,M для каждого множестваBn+i , 0 ≤ i < k, верно соотношение ψ1 Rψ2 ∈/ Bn+i . А отсюдаследует, что ψ1 ∈/ Bn+i для любого i, 0 ≤ i < k.Тогда по индуктивному предположениюtr |n+i |= ψ2 и tr |n+i 6|= ψ1 для любого i, 0 ≤ i < k,tr |n+k 6|= ψ2 .rrrtr |n 6|= ψ1 tr |n+1 6|= ψ1tr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1tr |n+k−1 6|= ψ1tr |n+k−1 |= ψ2- y- yn+2А это означает, что tr |n 6|= ψ1 Rψ2 .tr |n+k 6|= ψ2- yn+k-r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.Вариант 2.
X(ψ1 Rψ2 ) ∈ Bn+k .Т. к. все вершины (sn+i , Bn+i ), 0 ≤ i < k не окрашены в цвет j,для каждого из множеств Bn+i , 0 ≤ i < k, верны соотношенияψ2 ∈ Bn+iиX(ψ1 Rψ2 ) ∈/ Bn+i .Тогда по определению графа Γϕ1 ,M для каждого множества/ Bn+i . А отсюдаBn+i , 0 ≤ i ≤ k, верно соотношение ψ1 Rψ2 ∈следует, что ψ1 ∈/ Bn+i для любого i, 0 ≤ i < k и ψ2 ∈/ Bn+k .Тогда по индуктивному предположениюtr |n+i |= ψ2 и tr |n+i 6|= ψ1 для любого i, 0 ≤ i < k,tr |n+k 6|= ψ2 .rrrtr |n 6|= ψ1 tr |n+1 6|= ψ1tr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1tr |n+k−1 6|= ψ1tr |n+k−1 |= ψ2- y- yn+2И во втором случае tr |n 6|= ψ1 Rψ2 .tr |n+k 6|= ψ2- yn+k-r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.Таким образом, если ψ1 Rψ2 ∈/ Bn , то tr |n 6|= ψ1 Rψ2 .В итоге, для любой формулы вида ψ1 Rψ2 и для любойвершины (sn , Bn ) нашего радужного маршрута верносоотношениеψ1 Rψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 Rψ2 .4.
Темпоральный оператор U.Для доказательства соотношенияψ1 Rψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 Rψ2применяются рассуждения, аналогичные тем, которые былииспользованы для исследования оператора R.Самостоятельно.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИЗавершив обоснование индуктивного перехода, мы тем самымзавершили доказательство первой части теоремы:M 6|= ϕ1⇑в графе Γϕ1 ,M существует хотя бы один радужный маршрут,исходящий из вершины v0 = (s0 , B0 ), в которой s0 ∈ S0 иϕ1 ∈/ B0 .Покажем, что в том случае, когда имеет место M 6|= ϕ1 , вграфе Γϕ1 ,M из некоторой вершины v0 = (s0 , B0 ), в которойs0 ∈ S0 и ϕ1 ∈/ B0 , исходит хотя бы один радужный маршрут.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИПусть M 6|= ϕ1 . Тогда в LTS M существует такая начальнаятрасса tr , для которой tr 6|= ϕ1 .
Рассмотрим эту трассу tr .Для каждого i, i ≥ 0, положимBi = {ψ : ψ ∈ FLSubϕ1 , tr |i |= ψ .}Согласно утверждению 4, все построенные множества Biявляются согласованными.Покажем, что последовательность пар(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . . , (tr [n], Bn ), (tr [n+1], Bn+1 ), . .
.образует искомый радужный маршрут в графе Γϕ1 .ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДействительно,1. Для любого n, n ≥ 0, верно tr [n] −→ tr [n + 1], поскольку tr— маршрут в LTS M.2. Для любого n, n ≥ 0 и для любой формулы Xψ ∈ XSubϕ1 ,верноXψ ∈ Bn ⇐⇒ ψ ∈ Bn+1посколькуXψ ∈ Bn ⇐⇒ tr |n |= Xψ ⇐⇒ tr |n+1 |= ψ ⇐⇒ ψ ∈ Bn+1 .3. tr [0] ∈ S0 (т. к. tr — начальная трасса в M) и ϕ1 ∈/ B0 (т. к.tr |0 6|= ϕ1 ).Значит, последовательность(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . .
, (tr [n], Bn ), (tr [n+1], Bn+1 ), . . .является маршрутом в графе Γϕ1 ,M , исходящим из нужнойвершины.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИ4. Осталось показать, что маршрут(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . . , (tr [n], Bn ), (tr [n+1], Bn+1 ), . . .является радужным.Рассмотрим произвольное число n, n ≥ 0 и произвольнуюформулу ψi ∈ URSubϕ1 .
Покажем, что существует такоеk, k ≥ 0, что вершина (tr [n + k], Bn+k ) окрашена в цвет i.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИОграничимся рассмотрением Until-формулы ψi = χ0 Uχ2 .(Для формул вида ψi = χ0 Rχ2 доказательство проведитесамостоятельно. )1. Если tr |n 6|= X(χ1 Uχ2 ), то X(χ1 Uχ2 ) ∈/ Bn , и,следовательно, вершина (tr [n], Bn ) окрашена в цвет j.2. А если tr |n |= X(χ1 Uχ2 ), то tr |n+1 |= χ1 Uχ2 . Тогдасуществует такое k, k ≥ 1, что tr |n+k |= χ2 . Поэтомуχ2 ∈ Bn+k , и вершина (tr [n + k], Bn+k ) окрашена в цвет j.Таким образом, вершины цвета j встречаются в нашеммаршруте бесконечно часто.
Поскольку ψi была произвольной(Until-Release)-формулой, это означает, что наш маршрут вграфе Γϕ1 ,M является радужным.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММНо как проверить, что из заданной вершины в графе Γϕ1 ,Mне исходит ни одного радужного маршрута?Ориентированный граф Γ называется сильно связным , еслидля любой пары вершин v и u в графе Γ существует маршрутиз v в u и маршрут из u в v .Всякий максимальный сильно связный подграф графа Γназывается компонентой сильной связности .Компоненту сильной связности графа (системы Хинтикки)Γϕ1 ,M будем называть радужной, если в ней содержатсявершины всех цветов.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММТеорема.Из вершины v в графе Γϕ1 ,M исходит радужный маршрут тогдаи только тогда, когда существует маршрут , ведущий извершины v хотя бы в одну из вершин хотя бы одной радужнойкомпоненты сильной связности.Доказательство.Самостоятельно.
Здесь все очевидно.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММИсходные данные: формула PLTL ϕ и LTSM = hAP, S, S0 , −→, ρi.1. Построить равносильную позитивную форму ϕ1 .2. Построить систему Хинтикки Γϕ1 ,M .3. Выделить множество подформул URSubϕ1 и раскраситьвершины графа Γϕ1 ,M .4. Выделить радужные компоненты сильной связности вграфе Γϕ1 ,M .5. Выделить множество V 0 всех вершин графа Γϕ1 ,M , изкоторых достижимы радужные компоненты сильнойсвязности.6. Выделить множество V 00 всех вершин (s0 , B0 ), для которойвыполняется s0 ∈ S0 , ϕ1 ∈/ B0 .7. Вычислить V = V 0 ∩ V 00 .Результат: M |= ϕ ⇐⇒ V = ∅.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММПример.ϕ = pUqLTS M:' $s1'- iξ(s1 ) = {p} 6&s0s2?i$ξ(s2 ) = {q}%yξ(s0 ) = {p}'s3&- iξ(s3 ) = {p} 6&$s4?iξ(s4 ) = {p}%%АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММПример.ϕ = F(pUq)1.
Позитивная форма ϕ1 = pUqFLSubϕ1 = {p, ¬p, q, ¬q, pUq, X(pUq)};XSubϕ1 = {X(pUq)};URSubϕ1 = {pUq}.АЛГОРИТМ ВЕРИФИКАЦИИ2. Строим систему Хинтикки Γϕ1 ,Mi{¬p, q}6' %s1s?2i'- i{p, ¬q,6{¬p, q}{p, ¬q}- ?is1's2ϕ1 , Xϕ1 }s0{p, ¬q}is0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }i&- i{p, ¬q} 64?sis3{p, ¬q}- is36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}i%АЛГОРИТМ ВЕРИФИКАЦИИ3. Раскрашиваем вершины системыΓ ϕ1 ,M{p, ¬q}y{¬p, q}6' %s1s?2y'- i{p, ¬q,6{¬p, q}- ?ys1's2ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }i&- i{p, ¬q} 64?sis3{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ4. Выделяем радужные компонентысильнойсвязности{p, ¬q}{¬p, q}y6' %s1s?2y'- i{p, ¬q,6{¬p, q}- ?ys1's2ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }i&- i{p, ¬q} 6?s4is3{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ5.
Выделяем вершины из которыхдостижимырадужные компоненты{p, ¬q}{¬p, q}y6' %s1s?2y'- y{p, ¬q,6{¬p, q}- ?is1's2ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }$ϕ1 , Xϕ1 }y&- i{p, ¬q} 6?s4is3{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&$ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ6. Ищем вершину (s0 , B) на которойопровергаетсяϕ1'{p, ¬q}{¬p, q}y6' %s1s?2y'- y{p, ¬q,6{¬p, q}- ?is1s2ϕ1 , Xϕ1 }$$ϕ1 , Xϕ1 }s0s0yy{p, ¬q}{p, ¬q,ϕ1 , Xϕ1 }&- i{p, ¬q} 6?s4is3ϕ1 , Xϕ1 }&{p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }s4?{p, ¬q}y%АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММОписанный здесь подход к верификации распределенныхпрограмм реализован в программно-инструментальной системеверификации SPIN .Модели параллельных взаимодействующих процессовописываются на языке PROMELA (Process Meta Language),снабжаются темпоральными спецификациями (PLTLформулами), а затем выполнимость этих формул проверяетсясистемой верификации SPIN .В системе SPIN применяется табличный алгоритмверификации моделей распределенных программ.
Дляповышения его эффективности используется ряд приемов:I проверка модели «на лету»;I редукции частичных порядков;I символьное представление данных и др.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММБолее подробно о системе верификации SPIN вам расскажутКонстантин Олегович СавенковиИгорь Владимирович Конновв курсе«Верификация программ на моделях»в весеннем семестре.КОНЕЦ ЛЕКЦИИ 22ЭКЗАМЕН СОСТОИТСЯ 11ЯНВАРЯ в 10 часов.КОНСУЛЬТАЦИЯ — 10 ЯНВАРЯв 15 часов..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
