Главная » Просмотр файлов » Лекции В.А. Захарова

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

Файл №1157993 Лекции В.А. Захарова (Лекции В.А. Захарова) 35 страницаЛекции В.А. Захарова (1157993) страница 352019-09-18СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 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), ò.

Характеристики

Тип файла
PDF-файл
Размер
14,68 Mb
Тип материала
Высшее учебное заведение

Список файлов лекций

Свежие статьи
Популярно сейчас
Почему делать на заказ в разы дороже, чем купить готовую учебную работу на СтудИзбе? Наши учебные работы продаются каждый год, тогда как большинство заказов выполняются с нуля. Найдите подходящий учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6455
Авторов
на СтудИзбе
305
Средний доход
с одного платного файла
Обучение Подробнее