Лекция 22. Задача верификации моделей программ. Подформулы Фишера-Ладнера... (1161892), страница 3

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

Ïîçèòèâíàÿ ôîðìà ϕ1 = p UqFLSubϕ1 = {p, ¬p, q, ¬q, p Uq, X(p Uq)};XSubϕ1 = {X(p Uq)};URSubϕ1 = {p Uq}.ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ2. Ñòðîèì ñèñòåìó Õèíòèêêè Γϕ1 ,M{p, ¬q}- ?is1's2's1'- i6{p, ¬q,ϕ1 , Xϕ1 }s0{p, ¬q}is0{p, ¬q,ϕ1 , Xϕ1 }6%s2?i$${¬p, q}ϕ1 , Xϕ1 }i?s4is3&- i6{p, ¬q} {p, ¬q}- is36%{p, ¬q}ϕ1 , Xϕ1 }&i{¬p, q}ϕ1 , Xϕ1 }s4?{p, ¬q}i%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ3. Ðàñêðàøèâàåì âåðøèíû ñèñòåìûΓ ϕ1 ,M{p, ¬q}- ?ys1's2's1'- i6{p, ¬q,ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }6%s2?y$${¬p, q}ϕ1 , Xϕ1 }i?s4is3&- i6{p, ¬q} {p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&y{¬p, q}ϕ1 , Xϕ1 }s4?{p, ¬q}y%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ4. Âûäåëÿåì ðàäóæíûå êîìïîíåíòûñèëüíîéñâÿçíîñòè{p, ¬q}- ?ys1's2's1'- i6{p, ¬q,ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }6%s2?y$${¬p, q}ϕ1 , Xϕ1 }i?s4is3&- i6{p, ¬q} {p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&y{¬p, q}ϕ1 , Xϕ1 }s4?{p, ¬q}y%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ5. Âûäåëÿåì âåðøèíû èç êîòîðûõäîñòèæèìûðàäóæíûå êîìïîíåíòû{p, ¬q}- ?is1's2's1'- y6{p, ¬q,ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }6%s2?y$${¬p, q}ϕ1 , Xϕ1 }y?s4is3&- i6{p, ¬q} {p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&y{¬p, q}ϕ1 , Xϕ1 }s4?{p, ¬q}y%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ6.

Èùåì âåðøèíó (s0 , B) íà êîòîðîéîïðîâåðãàåòñÿϕ1{p, ¬q}- ?is1's2's1'- y6{p, ¬q,ϕ1 , Xϕ1 }y{¬p, q}6%s2?y$${¬p, q}ϕ1 , Xϕ1 }s0s0yy{p, ¬q}{p, ¬q,ϕ1 , Xϕ1 }?s4is3&- i6{p, ¬q} {p, ¬q}ϕ1 , Xϕ1 }&{p, ¬q}- ys36%ϕ1 , Xϕ1 }s4?{p, ¬q}y%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÎïèñàííûé çäåñü ïîäõîä ê âåðèôèêàöèè ðàñïðåäåëåííûõïðîãðàìì ðåàëèçîâàí â ïðîãðàììíî-èíñòðóìåíòàëüíîé ñèñòåìåâåðèôèêàöèè SPIN .Ìîäåëè ïàðàëëåëüíûõ âçàèìîäåéñòâóþùèõ ïðîöåññîâîïèñûâàþòñÿ íà ÿçûêå PROMELA (Process Meta Language),ñíàáæàþòñÿ òåìïîðàëüíûìè ñïåöèôèêàöèÿìè (PLTLôîðìóëàìè), à çàòåì âûïîëíèìîñòü ýòèõ ôîðìóë ïðîâåðÿåòñÿñèñòåìîé âåðèôèêàöèè SPIN . ñèñòåìå SPIN ïðèìåíÿåòñÿ òàáëè÷íûé àëãîðèòìâåðèôèêàöèè ìîäåëåé ðàñïðåäåëåííûõ ïðîãðàìì.

Äëÿïîâûøåíèÿ åãî ýôôåêòèâíîñòè èñïîëüçóåòñÿ ðÿä ïðèåìîâ:Iïðîâåðêà ìîäåëè ¾íà ëåòó¿;Iðåäóêöèè ÷àñòè÷íûõ ïîðÿäêîâ;Iñèìâîëüíîå ïðåäñòàâëåíèå äàííûõ è äð.ÊÎÍÅÖ ËÅÊÖÈÈ 22.

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

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