lect09 (К. Савенков - Верификация программ на моделях (2010))

Верификация программна моделяхЛекция №9Выразительная мощность LTL.Корректная абстракция графов программ.Отношение моделирования (симуляции).Константин Савенков (лектор)План лекции• Выразительная мощность LTL:– сравнение с автоматами Бюхи,– сравнение с CTL*, CTL,– Общая картина.• Корректная абстракция графов программ:– Отношение слабого моделирования,– Сильное моделирование.Выразительная мощность LTLпо сравнению с конструкциями never• Автомат Бюхи описывает ω-регулярныйязык:– Aω, где А – регулярный язык,– AB, где А – регулярный, а В – ω-регулярныйязык,– АUB, где A и B – ω-регулярные языки;• при помощи never можно описать любойω-регулярный автомат над словами.Выразительная мощность LTLпо сравнению с конструкциями never• LTL описывает подмножество этого языка:– всё, выразимое в LTL, может быть описано припомощи never,– при помощи never можно описать свойства,невыразимые на LTL.• Теорема: Добавление одного кванторасуществования над однимпропозициональным символом расширяетвыразительные способности LTL до всех ωрегулярных автоматов над словами.Пример свойства, не выразимого наLTL• (p) может быть истинным после выполнения системойчётного числа шагов, но никогда не истинно посленечётного.• []X(p) не подходитtruep• p && [](p -> X!p) && [](!p -> Xp) – такжене подходит (здесь p всегда истинно после чётныхшагов)p!p• ∃t.t&&[](t->X!t)&&[](!t->Xt)&&[](!t->!p)– то, что надо:true!pСравнение LTL с другими логиками• LTL-формула описывает свойство, которое должно выполнятьсяна всех вычислениях, начинающихся из исходного состояниясистемыграмматика:Операторы:!логическое отрицание&&логическое И||логическое ИЛИXв следующем состоянииUсильный untilUслабый until<>рано или поздно[]всегдаСерым отмечены операторы,которые можно вывести из других:φ1 || φ 2<> φ[] φφ 1 U fi2========!(! φ 1 && ! φ 2)true U φ!<> φ[] φ 1 || (φ 1 U φ 2)пропозициональные формулы:p!f(f)f && ff || fтемпоральные формулы:f!φ(φ)φ && φφ || φXφφUφ<> φ[] φp – некоторый пропозициональный символf – некоторая пропозициональная формулаφ – некоторая темпоральная формулаЛогика СTL*• Логика ветвящегося времени:– использует кванторы ∀ и ∃,– использует F вместо <> и G вместо [].Операторы:!логическое отрицание&&логическое И||логическое ИЛИEсуществует путьАдля всех путейXв следующем состоянииUuntil (сильный)Fрано или поздноGвсегдаСерым отмечены операторы,которые можно вывести из других:φ 1 || φ 2AφFφGφ========!(! φ 1 && ! φ 2)!E ! φtrue U φ!F φформулы состояния: p!f(f)f && ff || fAφEφформулы пути:f!φ(φ)φ && φφ || φXφφUφFφGφp – некоторый пропозициональный символf – некоторая формула состоянияφ – некоторая формула путиЛогика СTL• Логика CTL – фрагмент логики CTL*, в котором под управлениемквантора пути (E или A) может находиться не более одногооператора X или U.Корректная CTL формула:p!φφ && φφ || φEXφE (φ U φ)A (φ U φ)p – некоторый пропозициональный символf – некоторая формула состоянияφ – некоторая формула путиМожно вывести:EF fAF fEG fAG fAX f==========E(true U f)A(true U f)!AF !f!EF !f!EX !fПримерВ LTL <>p означает:A<>pдля всех вычислений, начинающихсяв исходном состоянии s0, выполняется <>pВ CTL можно выразить:EF(p)существует вычисление, для котороговыполняется <>pAF(p)для всех вычислений выполняется <>pAG(p)для всех вычислений p – инвариантEG(p)существует вычисление, для котороговыполняется p – инвариантитд.Выразительные возможности CTL* и CTL• CTL* и CTL описывают подмножества ω-регулярныхавтоматов над деревьями– автоматы над деревьями более выразительны, чемавтоматы над словами (CTL-формула выполнима надереве трасс, а не на одной трассе);– CTL и LTL являются подмножествами CTL*;– CTL и LTL не сравнимы по выразительной мощности(пересекаются, но не включают);– на LTL можно описать свойства, не выразимые на CTL:• CTL не позволяет описать свойства вида []<>(p),• при помощи *+<>(p) в LTL задаются ограничениясправедливости;CTLLTL– на CTL можно описать свойства, не выразимые на LTL:• на LTL нельзя описать свойства вида AGEF(p),• AGEF(p) используется для описания свойства reset: из любогосостояния система может перейти в нормальное.Выразительная мощностьМодальное µ-исчисление,Автоматы над ω-деревьямиАвтоматы над ω-словами,автоматы Бюхи,конструкции never,∃LTLCTL*CTLLTLLTL без XКорректность абстракцииграфов программСхема понятийСистема(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремениКорректность моделированияграфов программPGабстракцияразвёрткаразвёрткаTS(PG)PG’абстракция(корректная)TS(PG’)• Необходимое и достаточное условие:– Программа PG’ корректно моделирует программуPG тогда и только тогда, когда система переходовTS(PG’) корректно моделирует систему переходовTS(PG).Абстракция графов программПример корректной абстракцииПрограмма:PG:PG’:00:x = 2;int x,y;0: x = 2;1: y = 3;2: while (x > 0) x <= 0:τ{3:y += 1;4:x -= 1;}5::x = 2;1:y = 3;x <= 0:τ22x > 0:τx > 0:τ3:y += 1;45:x -= 1;45:x -= 1;Абстракция графов программПример некорректной абстракцииTS(PG):PG:PG’:TS(PG’):0,0,0000,0,0x = 2;:x = 2;1,2,01y = 3;2,2,3:y = 3;2,1,4x>0 x<=0:τ2x > 0:τx-=1;x > 02,2,0y+=1;y+=1;4,2,4324:x-=1;3x>03,1,13,2,0y+=1;y+=1;:y += 1;4,2,14,1,2:x-=1;x -= 1;2,0,22,0,5!(x > 0)!(x > 0)5,0,52,1,1x-=1;x > 0x > 0:τ:y += 1;4,1,5x -= 1;1x<=0:τ3,1,43,2,3x = 2;:x = 2;545,0,2Абстракция графов программПример корректной абстракцииTS(PG):PG:PG’:TS(PG’):0,0,0000,0,0x = 2;:x = 2;1,2,01y = 3;2,2,3x>0 x<=0:τ2x > 0:τx-=1;x > 0y+=1;y+=1;4,2,43:τ2x -= 1;42,2,33,2,33:x-=1;3,1,4y+=1;4,2,4:x-=1;4,1,5x -= 1;2,0,52,0,5!(x > 0)5,0,5x>0y+=1;:y += 1;42,1,4x-=1;x > 0:τ:y += 1;4,1,5y = 3;:y = 3;3,1,43,2,31,2,01:y = 3;2,1,4x = 2;:x = 2;!(x > 0)555,2,35,1,45,0,5Абстракция графов программПример корректной абстракцииTS(PG):PG:PG’:TS(PG’):0,0,0000,0x = 2;:x = 2;y = 3;1,2,0y = 3;2,2,3:y = 3;2,1,4x>0 x<=0:τ2x > 0:τx-=1;x > 0:y = 3;1:τ1,313,1,43,2,3y+=1;y+=1;4,2,4y+=1;y+=1;:τ3:y += 1;4,1,5x -= 1;1,44:x-=1;2,422,5:y+=1;2,0,51,5!(x > 0)5,0,5533,33,43,5Неформальное определениеPG  Loc, Act , Effect , , Loc0 , g0PG '  Loc' , Act ' , Effect ' , ' , Loc0 ' , g0 'Будем говорить, что PG’ моделирует PG, если1.

В PG’ присутствуют переменные, соответствующиенаблюдаемым переменным PG,2. Все действия PG, влияющие на наблюдаемыепеременные, отражены в модели,3. Модель корректно воспроизводит возможныепоследовательности изменения значенийнаблюдаемых переменных PG.Отношение (слабого) моделирования(слабой симуляции)• Будем говорить, что точки l0 и l’0 связаныотношением слабого моделирования S, таким, что(l0,l0’)∈S тогда и только тогда:g:ag:al0 l1 : a     l1 ' , l0 ' l1 '   l1 ,  Loc (l ' )   SСлабая симуляция!aabbaτbДостаточное условие корректности• Будем говорить, что PG’ моделирует PG, если Loc : Loc  Loc' , Loc0 '   ( Loc0 )g0 '  g0 |VarPG ' Act : Act  Act ' Var : VarPG  VarPG '   a  Act , v Var PG ,  Act (a )    Var (v )     Effect (a, v )  va  Act , v Var PG ,  Act (a )    Var (v )     Effect ' ( Act ( a ), Var ( v ))  Effect ( a, v )  va  Act '\ Act , v VarPG  VarPG ' , Effect ' (a, v )  v а точки Loc0 и α(Loc0’) связаны отношениемслабой симуляции S:g:ag:al0 l1 :  Act (a )     l1 ' , l0 ' l1 '   l1 ,  Loc (l ' )   SСлабое моделирование• Отношение слабого моделирования несохраняет количество шагов междусостояниями:00:x = 2;:y = 3;1:y = 3;21• Не сохраняются свойства, не инвариантныек прореживаниюСильное моделирование• Для сохранения отношения сильногомоделирования необходимо сохранятьколичество шагов программы междуизменением состояния00:x = 2;1:τ1:y = 3;2:y = 3;2Сильное моделирование• С добавлением переменных и операторов вмодели тоже не всё просто:0:y = 3;10:count += 1;Сильноемоделированиенарушается2:y = 3;01:atomic{y = 3;count += 1;}1СильноемоделированиесохраняетсяЧто дальше• Будет ещё две лекции (И.

Коннов):– алгоритмы верификации в SPIN,– хранение пространств состояний.• Сегодня (12 апреля) будет выслано ещё однозадание практикума– проверка свойств модели из задания №3,– дедлайн 26 апреля.• 28 апреля – выставление зачёта по практикумудля АСВК (с приёмом последнего задания).• Экзамен – 7-11 июня– перед экзаменом будет консультация.Оценки по курсу• Оценка за курс:– Оценка по практикуму – 2 = 0..3 балла +– Оценка за экзамен (0..3 балла) +– Оценка за летучки (-1..1 балл).• «Слитые» контрольные – в виде доп.вопросов на экзамене.• Автоматы будут– Критерии пока не определены.Спасибо за внимание!Вопросы?.