lect08 (1158549)

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

Текст из файла

Верификация программна моделяхЛекция №8Логика линейного времени (LTL).Константин Савенков (лектор)План лекции• Логика линейного времени (LTL)• Свойства, инвариантные к прореживанию• Связь между LTL и автоматами Бюхи/ конструкциями never• Применение LTL в системе Spin• Практические приёмы формулированиясвойств на LTLПроверка свойств при помощиавтоматов Бюхи(напоминание)• При помощи автомата Бюхи можно описатьнаблюдаемое поведение программы итребования к нему,• Проход автомата соответствует наблюдаемомувычислению (трассе) программы,• Определение допускаемости проходапозволяет рассуждать о выполнении илинарушении требований (свойствправильности).• Задавать свойства правильности при помощиавтоматов неудобно.Безопасность и живучесть• Безопасность(напоминание)– Любое свойство безопасности можно проверить, исследуясвойства отдельных состояний модели;– если свойство безопасности нарушено, всегда можноопределить достижимое состояние системы, в котором ононарушается;– для проверки свойств безопасности требуется генерироватьсостояния системы и для каждого из них проверять свойство;– при проверки таких свойств можно обойтись безтемпоральных логик и автоматов Бюхи.• Живучесть– Для проверки свойств живучести необходимо рассматриватьпоследовательности состояний (конечные и бесконечныепроходы соотв.

автомата Бюхи);– для проверки свойств используются другие, более сложныеалгоритмы;– свойства удобно описывать при помощи формултемпоральной логики, а проверять – при помощи автоматовБюхи.Примеры темпоральных свойств• p всегда истинно;• p рано или поздно станет всегда ложным;• p всегда рано или поздно станет ложнымхотя бы ещё один раз;• p всегда ведёт к ¬q;• p всегда ведёт к тому, что рано или поздностанет истинным q.Темпоральная логика LTL• Ясный, лаконичный и непротиворечивый способописания требований к программам;• В явном виде время не присутствует, однакорассуждения ведутся в терминах «никогда»,«всегда», «рано или поздно», которыепредставлены в виде темпоральных операторов.• Мы рассматриваем темпоральную логикулинейного времени – LTL.

С её помощью можноописывать свойства, которым должныудовлетворять линейные последовательностинаблюдаемых состояний – трассы.• LTL предложена Амиром Пнуэли (Amir Pnueli) вконце 70-х.Темпоральная логика LTL• Семантика LTL определена на бесконечныхпроходах автомата Бюхи.• Пример:Синтаксис Spin– ((a ≠ b)(a = b))– #define a !=b P#define a == b Q[]((a != b) -> <>(a == b))– всегда, когда выполняется ( a!=b ), в концеконцов становится истинным (a == b).– как правило, формула описывает не однуконкретную трассу, а класс трасс.Формулы LTL• Могут использоваться для описания каксвойств живучести, так и безопасности• LTL = пропозициональная логика+ темпоральные операторы• Формула LTL f ::=– p, q, … - свойства состояний, включая true и false,– ( f ) – группировка при помощи скобок,– f – унарные операторы,– f1 f2 – бинарные операторы.Операторы LTL• Унарные:– ([]) всегда (в будущем),– (<>) рано или поздно,– (Х) в следующем состоянии,– ¬ (!) логическое отрицание;• Бинарные:( p∨q)– U (U) пока,– ∧(&&) логическое И,– ∨(||) логическое ИЛИ,(p q)∧(q p)– (->) логическая импликация,– (<->) логическая эквивалентность.Выполнимость формул• Последовательность состояний проходаs0 , s1 , s2 , s3 ,...• Набор пропозициональных формул p, q:i, i  0, и p, определено sip• Семантика LTL:s0fs0sisi[] ffj, j  i : s jj, j  i : s jsiXfsi 1sisi+1ffffСлабый и сильный untilслабый: sieWfсильный: si(Spin)eUfsif  ( sie  si 1 (eWf ))j, j  i : s jfk , i  k  j : sksiesjeeefиeПрактически важные следствияe W false  []etrueU f  eeW f  []! f  eUfПримерыppps0pppsisi+1pqppppsn-1snq | [] p |  p | [] p | []q |  q | [] q | pUq  | []( pUq)  | []( pWq) | qUp  | []( qUp) | qWp | []qWpЦикличность и стабильность• Свойством цикличности называется любаятемпоральная формула, котораяпредставима в видеp, где p – формулана состоянии;• Свойством стабильности называется любаятемпоральная формула, котораяпредставима в видеp, где p – формулана состоянии.Распространённые LTL-формулыФормулаОписаниеТип[] pвсегда pинвариант pрано или поздно pгарантияp   qесли p, то рано или поздно qоткликp  qUrесли p, то q, затем rприоритет[] pвсегда рано или поздно будет p[] pрано или поздно всегда будет p p   pесли рано или поздно p,то рано или поздно qцикличность(прогресс)стабильность(бездействие)корреляцияЭквивалентные преобразования![] p! p!( pUq)!( pWq )[]( p  q)( p  q)pW ( q  r )( p  q)WrpU ( q  r )( p  q)Ur[]( p  q)[]( p  q)! p[]! p! qW (! p!q)! qU (! p!q)[]p  []q p  q(pWq)  ( pWr)(pWr)  ( qWr)(pUq)  ( pUr)(pUr)  ( qUr)[] p  []q[]p  []qПримеры темпоральных свойств[]p<>[]!p• p всегда истинно;• p рано или поздно станет всегда ложным;• p всегда рано или поздно станет ложнымхотя бы ещё один раз;[]<>!p• p всегда ведёт к ¬q;[](p->!q)• p всегда ведёт к тому, что рано или поздностанет истинным q.[](p-> <>q)Правильная интерпретацияформул LTLLTL: b1  !b2Ub2   []! a31.2.3.4.Пусть b1 всегда ложно, pq означает, что !p∨q;формула выполняется.Пусть b1 стало истинно,но b2 всегда ложно;формула выполняется.Пусть b1 стало истинно,затем – b2, однако a3всегда ложно; формулавыполняется.Пусть b1 стало истинно,затем – b2, затем – a3;формула невыполняется.!b1времяb1!b2b2b1время!b2!a3b2b1времяa3!b2!a3времяПравильная интерпретацияформул LTLLTL:1.b1   b2 Пусть b1 и b2 всегдаложно; формулавыполняется.!b1времяb22.3.Пусть и b1, и b2становятсяистинными; формулавыполняется.Пусть b1 становитсяистинным, но b2всегда ложно;формула невыполняется.b1!b2время!b1b1!b1!b2времяПравильная интерпретацияформул LTLLTL:1.[]b1   b2 Пусть b1 и b2 всегдаложно; формулавыполняется.!b1времяb12.3.Пусть и b1, и b2бесконечночередуются; формулавыполняется.Пусть b2 становитсяистинным толькоодин раз; формула невыполняется.!b2b1b2!b1!b2b2!b1!b2!b1!b1время!b2b1b2!b1b1!b2!b1!b2времяОписание требований при помощиLTL“p приводит к q”• p -> q– нет темпоральных операторов, т.е.применяется только к первому состоянию;– выполняется только если !p∨q в первомсостоянии, остальная трасса нерассматривается;– не подходит;– нужно использовать темпоральныеоператоры.Описание требований при помощиLTL“p приводит к q”• [] p -> q– правила приоритета! [] применяется только к p;– означает ([]p) -> q;– не подходит;– нужно расставить скобки.Описание требований при помощиLTL“p приводит к q”• [] (p -> q)– проверяем условие во всех состояниях, нопричинно-следственная связь между p и qотсутствует;– выполняется, только если ! p∨q во всех состояниях;– не подходит;– нужно описать, что p является причиной q.Описание требований при помощиLTL“p приводит к q”• [] (p -> <>q)– уже лучше;– тем не менее, формула выполнима, если qстановится истинным в том же состоянии, что и p –причинно-следственная связь отсутствует;– не подходит;– нужно описать, что q не может произойти раньшеследующего шага после p.Описание требований при помощиLTL“p приводит к q”• [] (p -> X(<>q))– практически то, что нужно;– формула выполнима, если p всегда ложно;– скорее всего, не подходит;– нужно описать, что p обязательно произойдёт иприведёт к q.Описание требований при помощиLTL“p приводит к q”• [] (p -> X(<>q)) && (<>p)– скорее всего, мы имели ввиду именно это;– несколько отличается от первоначального p->q;– LTL позволяет выразить множество различныхоттенков свойства;– подойдёт ли такое свойство для моделипараллельной программы?Оператор neXt• Оператор X нужно использовать аккуратно:– с его помощью делается утверждение овыполнимости формулы на непосредственныхпотомках текущего состояния;– в распределённых системах значение оператора Хнеочевидно;– поскольку алгоритм планирования процессовнеизвестен, не стоит формулироватьспецификацию в предположении о том, какоесостояние будет следующим;– стоит ограничиться предположением осправедливости планирования.Свойства, инвариантные кпрореживанию• Пусть φ – трасса некоторого вычисления надпропозициональными формулами P,– по трассе можно определить, выполняется ли наней темпоральная формула,n1 n 2 n 3– трассу можно записать в виде   1  2 3 ...

,где значения пропозициональных формул накаждом интервале совпадают.• Обозначим E(φ) набор всех трасс,отличающихся лишь значениями n1, n2, n3(т.е. длиной интервалов)– E(φ) называется расширением прореживания φ.Расширение прореживанияx=1p: (x == mutex)q: (x != y)трасса φ1 E(φ)printfmutex--x==1y==0mutex==0x==1y==0mutex==0p!p!pp!qqqqp!pp!pp!qqqq!qx==0bit x,y;byte mutex;y==0active proctype A()mutex==0{x = 1;(y == 0) ->mutex++;printf(“%d\n”, _pid);mutex--;x = 0}трасса φ(y==0) mutex++x==1x==1y==0y==0mutex==1 mutex==1x=0x==1y==0mutex==0x==0y==0mutex==0p!ppqq!qСвойства, инвариантные кпрореживанию• Свойство φ, инвариантное к прореживанию, либоистинно для всех трасс из E(φ), либо ни для однойиз них:f  v  E ( ), vf• истинность такого свойства зависит от порядка, вкотором пропозициональные формулы меняютсвои значения, и не зависит от длины трассы;• Теорема: все формулы LTL без оператора Xинвариантны к прореживанию.• Более того, в рамках LTL без X можно описать всесвойства, инвариантные к прореживанию.Связь между LTLиавтоматами Бюхи(конструкциями never)Связь LTL с автоматами Бюхи• Удобно проверять допустимость трасс длянекоторого автомата Бюхи;• Удобно описывать свойства правильности припомощи темпоральных формул;• Что дальше?• Теорема: Для всякой формулы LTL f существуетавтомат Бюхи, который допускает те и толькоте прогоны, которым соответствуют трассы, накоторых выполнима f.• Пример: формуле <>[]p соответствуетавтоматtrues0ps1pПереход от LTL к автоматам• Привести свойство правильности LTL к форме neverязыка Promela достаточно просто: нужно построитьотрицание формулы LTL f и поместить его в телоnever:– f выполняется на всех вычислениях – !f не выполняется ни на одном вычислении – автомат {!f} не допускает ни одного прохода,полученного в результате синхронного выполнения ссистемой.![] p  []![] p  []! ptrues0!ptrues1Примеры!p||q• p -> qtrue!p||q• []p -> qtruetrue!ptrue• [](p -> q)!p||qПримерыtrue• [](p -> <>q)true!p||q!pqtruetrue• [](p -> X<>q)!p&&qq!p&&ptrueqИ, наконец…• [](p -> X<>q)&&(<>p)true!p&&qptruep&&qtruetrueq !p&&q !pptrue!ptruetrue• &&(<>p)!pptrueptrue!p!qОтрицания формул LTLФормулу LTL всегда можно переписать в таком виде,что отрицания будут появляться только передпропозициональными символами• •  – по определению логической импликации• <>!(!p || <>q) – ![]p эквивалентно <>!p• <>(p && !<>q) – По правилу ДеМоргана• <>(p && []!q) – !<>q эквивалентно []!qИ, наконец…• &&(<>p)– )!p– <>!(!p || (X<>q))ptrue– <>(p && !(X<>q))– <>(p &&(X[]!p))ptrue!p!qИспользуем Spin длятрансформации формул LTL> ./spin -f '<>[]p'never {/* <>[]p */T0_init:if:: ((p)) -> goto accept_S4:: (1) -> goto T0_initfi;accept_S4:if:: ((p)) -> goto accept_S4fi;}> ./spin -f `!<>[]p'never {/* !<>[]p */T0_init:if:: (! ((p))) -> gotoaccept_S9:: (1) -> goto T0_initfi;accept_S9:if:: (1) -> goto T0_initfi;}true T0_initps4!ptrue T0_inittrues9pПравила синтаксиса> ./spin -f `([]p -> <> (a+b <= c) )'#define q (a+b <= c)Вводим строчные макроопределениядля всех булевых подформул> ./spin -f `[] (p -> <> q)'never {/* [] (p -> <> q) */T0_init:if:: (((! ((p))) || ((q)))) -> goto accept_S20:: (1) -> goto T0_S27fi;accept_S20:if:: (((! ((p))) || ((q)))) -> goto T0_init:: (1) -> goto T0_S27fi;accept_S27:if:: ((q)) -> goto T0_init:: (1) -> goto T0_S27fi;T0_S27:if:: ((q)) -> goto accept_S20:: (1) -> goto T0_S27:: ((q)) -> goto accept_S27fi;}Следим за приоритетомоператоровLTL для проверки правильности припомощи Spinint x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}Ограничено ли значение x?> ./spin -f `[] (x > 0 && x <= 100)'tl_spin: expected ')', saw '>'tl_spin: [] (x > 0 && x <= 100)----------------^>Синтаксическая ошибка!LTL для проверки правильности припомощи Spinint x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}#define p (x > 0 && x <= 100)> ./spin -f `[] p'never {/* []p */accept_init:T0_init:if:: ((p)) -> goto T0_initfi;}pФормула синтаксически корректна, но мыже будем проверять её невыполнимость!LTL для проверки правильности припомощи Spinint x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}#define p (x > 0 && x <= 100)> ./spin -f `![] p'never {/* ![]p */T0_init:if:: (! ((p))) -> gotoaccept_all:: (1) -> goto T0_initfi;accept_all:skip}true!ptrueТо, что ![]p не может быть выполнено,означает, что []p не может бытьнарушено (нет ни одного контрпримера)LTL для проверки правильности припомощи Spinint x = 100;#define p (x > 0 && x <= 100)active proctype A(){do:: x%2 -> x = 3*x + 1od> ./spin -a ltl1.pml}> gcc -o pan pan.cactive proctype B()> ./pan -a{(Spin Version 5.1.4 -- 27 January 2008)do+ Partial Order Reduction:: !x%2 -> x = x/2Full statespace search for:never claim+odassertion violations+ (if within scope of claim)}acceptancecycles+ (fairness disabled)never {/* ![]p */invalid end states- (disabled by never claim)T0_init:...if:: (! ((p))) -> goto accept_all:: (1) -> goto T0_initfi;accept_all:skip}Ещё один примерint x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}Пусть#define p (x == 1)Выполнимо ли свойство []<>p?Даже в таком простом случаеметод пристального взглядаперестаёт работатьДля проверки неизбежности []<>pпроверяем невозможность![]<>p<>!(<>p)<>[]!pLTL для проверки правильности припомощи Spinint x = 100;#define p (x == 1)> ./spin -t -c ltl2.pmlactive proctype A()proc 0 = Aproc 1 = B{Never claim moves to line 18[(!((x==1)))]do[(!((x==1)))]:: x%2 -> x = 3*x + 1 Never claim moves to line 23<<<<<START OF CYCLE>>>>>odspin: trail ends after 3 steps}------------active proctype B()final state:{------------#processes: 2dox = 100:: !x%2 -> x = x/23:proc 1 (B) line 11 "ltl2.pml" (state 3)od3:proc 0 (A) line5 "ltl2.pml" (state 3)}3:proc - (:never:) line 22 "ltl2.pml" (state 9)never {/* ![]<>p */ 2 processes createdT0_init:>if:: (! ((p))) -> goto accept_S4:: (1) -> goto T0_initfi;accept_S4:> ./spin -a ltl1.pmlif> gcc -a pan pan.c:: (! ((p))) -> goto accept_S4> ./pan -apan: acceptance cycle (at depth 2)fi;pan: wrote ltl2.pml.trail}Практические приёмыописания свойств на LTLПрактические приёмы описаниясвойств на LTL• Выполнимость формулы LTL проверяетсятолько для первого состояния в трассе• Темпоральные операторы управляютпроверкой выполнимости своих аргументов• Сложное свойство можно (и нужно!)строить как суперпозицию простых• Суперпозиция темпоральных операторовне ограничивает диапазон действия«вложенного» оператора.Выполнимость формул LTL• Выполнимость формулы LTL определена ипроверяется для одного (первого)состояния трассы• Распространение свойств на другиесостояния управляется темпоральнымиоператорами• Единственный оператор, который можетограничить сверху проверку выполнимостиформулы – UntilСуперпозиция формул LTL• Составлять сложные формулы LTL нужнометодом суперпозиции простых формул• Внешняя формула задаёт, на каких участкахвычислений будет проверятся подформула• Подформула задаёт свойства, проверяемыедля участков вычислений• Суперпозиция темпоральных операторовне ограничивает диапазон действия«вложенного» оператора.Пример• В ходе одного вызова функции F() x всегда не превышает 3.где проверяем (g)что проверяем(f)• φ = g(f)• Что проверяем?– в синтаксисе LTL нет таких символов!#define a x <= 3 – определяемпропозициональный символf = []a – вроде бы точно описывает свойство f– f = x <= 3––Пример• В ходе одного вызова функции F() x всегда не превышает 3.где проверяем (g)что проверяем(f)• φ = g(f)• Где проверяем?– #define lab_f P@f_call – поставим метку на вызов f– g = [](lab_f -> f) – не то, проверяем для всегоучастка пути за первым вызовом Ff_call f_entryf_returnf_call f_entryf_return– #define f_b P@f_entry – нужно проверять свойство#define f_e P@f_return внутри тела функции– g = [](f_b -> (f U f_e)) – похоже на правду,проверяем от входа в функцию до выхода из неёПример• В ходе одного вызова функции F() x всегда не превышает 3.где проверяем (g)что проверяем(f)• φ = g(f)• Подставляем одно в другое– φ = [](f_b -> ([]a U f_e))f_bПроверяемвыполнимость φПроверкавыполнимости Uf_eПроверкавыполнимости []aПроверкавыполнимости a– зона действия [] по определению не ограничивается Until!– φ = [](f_b -> (a U f_e))– правильная формулаПомощь в формулировке свойствБаза шаблонов темпоральной логикиhttp://patterns.

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

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

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