Лекция 3. Системы переходов (LTS). Корректность и адекватность LTS модели (К. Савенков - Верификация программ на моделях (2012))

Верификация  программ  на  моделях  Лекция  №3  Системы  переходов  (LTS).  Корректность  и  адекватность  LTS  модели.  Константин  Савенков  (лектор)  Контрольная работа•  15 минут•  3 вопроса: 1 сложный (10 баллов) + 2простых (по 5 баллов)•  Эти баллы не связаны с баллами практикума•  Оценка–  0..9 баллов – не засчитывается, доп. вопросы потеме на экзамене; если так по большинствуконтрольных, то -1 балл к оценке за курс,–  10..19 баллов (формально правильные краткиеответы) – ОК,–  20 баллов (развёрнутый ответ, демонстрирующийпонимание) +1 балл; если таких много, то +1 коценке за курс => автоматПлан лекции• • • • • • • Система  понятий,  используемых  в  курсе  Размеченные  системы  переходов  (LTS)  Недетерминизм  систем  переходов  Пути,  вычисления,  трассы  Свойства  линейного  времени  Корректность  модели  Адекватность  модели  Итоги  прошлой  лекции  •  Свойства  проверяются  на  состояниях  и  их  последовательностях  •  Чтобы  перебирать  меньше  состояний,  исследуется  не  исходная  система,  а  её  модель  •  Модель  должна  быть  простой,  корректной  и  адекватной  •  В  этом  случае  из  правильности  модели  следует  правильность  программы  Строго  говоря…  Если  мы  хотим  доказать,  что  после  проверки  правильности  на  модели  в  программе  нет  ошибок,  то  все  эти  понятия  стоит  сформулировать    более  строго  Строго  говоря,  всё  должно  быть  так:  Система  (программа)  (описание)  корректна  Модель  (описание)  Система  (система  переходов)  корректна  Модель  (система  переходов)  Система  (трассы)  корректна  Модель  (трассы)  адекватна  адекватна  Требования  Свойства  линейного  времени  Различные  представления  программы  t   t   l  t   l   l  l   t   l  l  t  int main(){printf(}Исходный  код  программы  Взлетает,непадает,приземляетсяТребования  Граф  программы  (ACFG)  □(TAKEOFF →(!FALL)U(LANDED))Размеченная  система    переходов  Множество  вычислений  l   l   l   t  l   t   t   l  l   l   l  l   l  Спецификация  Допустимые  (линейного  времени)   последовательности  атомарных  высказываний  Множество  трасс  l  =  T  t  =  T  t  l  t  Язык  допустимых  трасс  Размеченные  системы  переходов  (LTS)  aTS = S , Act, ⎯⎯→, I , AP, L•           S        –  множество  состояний,  •         Act                –  множество  действий,    τ    –  невидимое  действие,  a•       ⎯      ⎯→                      ⊆            S        ×        Act                  ×        S      –  тотальное  отношение  переходов,  •         I      ⊆            S      –  множество  начальных  состояний,  •       AP                –  множество  атомарных  высказываний,  •       L        :      S        →              2      AP          –  функция  разметки.

     S          –  конечное  или  счётное  множество,      Act                    –  конечное  Нотация:    aa0s, a0 , s' ∈ ⎯⎯→≡ s ⎯⎯→s'Пример  LTS  0,?,?  0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:int x = 2;1,2,?  int y = 0;2,2,0  x > 02,1,1  x -= 1;3,2,0  3,1,1  y += 1;y += 1;Состояние:  (счётчик,  x,  y)  x > 04,2,1  4,1,2  x -= 1;2,0,2  !(x > 0)5,0,2  Пример  LTS  0,?,?  0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:Sint x = 2;1,2,?  a⎯⎯→int y = 0;2,2,0  x > 02,1,1  x -= 1;3,2,0  x > 03,1,1  y += 1;y += 1;Состояние:  (счётчик,  x,  y)  S × Act × S4,2,1  4,1,2  x -= 1;I ⊆SL2,0,2  !(x > 0)5,0,2  ⎧cnt = 0, cnt = 1,...⎫⎪⎪AP = ⎨ x = 0, x = 1,...

⎬⎪ y = 0, y = 1,... ⎪⎩⎭Что  включать  в  состояние  •  Набор  атомарных  высказываний     APопределяется  свойствами,  которые  нужно  проверить  •  Изменение  состояния  связано  с  изменением  выполнимости  хотя  бы  одного  атомарного  высказывания  •  Исходя  из  этого  мы  определяем,  что  включать  в  состояние  программы  •  Главное  –  не  «потерять»  ни  одного  изменения  атомарных  состояний  Пример  LTS  0,?,?  0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:Sint x = 2;1,2,?  a⎯⎯→int y = 0;2,2,0  x > 02,1,1  x -= 1;3,2,0  x > 03,1,1  y += 1;y += 1;Состояние:  (счётчик,  x,  y)  S × Act × S4,2,1  4,1,2  x -= 1;I ⊆SL2,0,2  !(x > 0)5,0,2  ⎧cnt = 0, cnt = 1,...⎫⎪⎪APAP= ⎨= {x = 0, x = 1,...} ⎬⎪ y = 0, y = 1,...

⎪⎩⎭Пример  LTS  x  =  ?  0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:Sint x = 2;x  =  2  a⎯⎯→int y = 0;x  =  2  x > 0x  =  1  x -= 1;x  =  2  x > 0x  =  1  y += 1;y += 1;Состояние:  (счётчик,  x,  y)  S × Act × Sx  =  2  x  =  1  x -= 1;I ⊆SLx  =  0  !(x > 0)x  =  0  AP = {x = 0, x = 1,...}Пример  LTS  x  =  ?  0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:Состояние:  (счётчик,  x,  y)  int x = 2;x  =  2  x -= 1;x  =  1  x -= 1;x  =  0  AP = {x = 0, x = 1,...}Что  включать  в  состояние?    В  дальнейшем  мы  будем  рассматривать  «универсальное»  определение  состояния,  достаточное  для  проверки  свойств  линейного  времени  и  локализации  их  нарушения  в  описании  программы  Совокупность  значения  счётчиков  управления  последовательных  процессов  и  переменных  программы  Пример  LTS  int p;process Prod() {while(1)1.1:if(p < 2)1.2:p += 1;}process Cons() {while(1)2.1:if(p > 0)2.2:p -= 1;}Состояние:  (счётчик  Prod,  счётчик  Cons,  p)  Часть  состояний  не  показана  (оператор  беск.

 цикла,  стартовые  состояния)  Prod            Cons  (1.1,2.1),0  p -= 1p < 2(1.1,2.2),1  (1.2,2.1),0  p += 1p > 0(1.1,2.1),1  p < 2p -= 1p < 2(1.2,2.1),1  p += 1p > 0(1.1,2.1),2  p > 0(1.1,2.2),2  (1.2,2.2),1  p += 1p -= 1Бесконечное  количество  вычислений,  однако    размеченная  система  переходов  конечна  Недетерминизм  •  В  ряде  ситуаций  шаг  может  сделать  любой  из  двух  процессов,  порядок  действий  не  определён  •  Недетерминизм  =  неопределённость  •  При  построении  LTS  рассматриваются  все  возможные  варианты  последовательности  действий  Недетерминизм  •  Вообще-­‐то  в  природе  довольно  мало  недетерминированных  процессов  •  Да  и  те  считаются  недетерминированными,  поскольку  физические  законы,  по  которым  выбирается  действие,  нам  не  известны  •  Недетерминизм  появляется,  как  только  мы  не  знаем  причин  выбора  действия  или  считаем  их  несущественными  Недетерминизм  •  Порядок  выполнения  Prod  и  Cond  на  конкретном  компьютере  детерминирован  и  определяется  алгоритмом  диспетчера  операционной  системы  и  состоянием  ресурсов  •  Для  проверки  правильности  программы  мы  решили  абстрагироваться  от  всего,  кроме  описания  двух  процессов  •  Итог  –  недетерминизм  очерёдности  выполнения  процессов  Подробнее  про  разные  виды  недетерминизма  –  ниже  Недетерминизм  –  это  фича!  •  Используется  для:  –  моделирования  параллельного  выполнения  процессов  в  режиме  чередования  (интерливинга)  •  позволяет  абстрагироваться  от  алгоритма  диспетчеризации  и  скорости  выполнения  процессов  Prod  Cons  ELF  System  board  Processor  Недетерминизм  –  это  фича!  •  Используется  для:  –  моделирования  прототипа  системы  •  не  ограничивает  будущую  реализацию  заданным  порядком  выполнения  операторов  или  конкретными  входными  данными  Недетерминизм  –  это  фича!  •  Используется  для:  –  построения  абстракции  реальной  системы  •  для  абстрагирования  от  деталей,  несущественных  для  проверки  свойств  и  для  построения  модели  по  неполной  информации  Недетерминизм  в  LTS  •  В  LTS  недетерминизм  проявляется  в  виде  состояний,  из  которых  можно  перейти  более  чем  в  одно  состояние  AP = {a}a  a  a  недетерминизм  действий  a  недетерминизм  атомарных  высказываний  строгие  определения  –  далее  Недетерминизм  в  LTS  •  В  LTS  недетерминизм  проявляется  в  виде  состояний,  из  которых  можно  перейти  более  чем  в  одно  состояние  ?  ?  может  произойти  одно    из  нескольких  действий  наблюдатель  не  может    отличить  два  состояния  строгие  определения  –  далее  Вспомогательные  определения  Прямые  потомки  вершины  s  по  действию  a  по  всем  действиям   Post ( s, a)aPost ( s, a ) = {s'∈ S | s ⎯⎯→ s' }, Post ( s) =s  s  a   a   b   c  a   a   b   c  a∈ActПрямые  предки  вершины  s  по  действию  a  по  всем  действиям  aPre ( s, a ) = {s'∈ S | s' ⎯⎯→s}, Pre ( s) = Pre( s, a)a∈Acta   a   b   c  a   a   b   c  s  s  Детерминизм  a•  Система          TS              =          S      ,      Act              ,    ⎯    ⎯→                  ,    I   , AP, Lдетерминирована  –  по  действиям,  тогда  и  только  тогда:  I ≤1 иPost ( s, a) ≤ 1, ∀s ∈ S , a ∈ Act–  по  атомарным  высказываниям,  тогда  и  только  тогда:  I ≤ 1 и Post ( s) ∩ {s'∈ S | L( s' ) = A} ≤ 1, ∀s ∈ S , A ∈ 2одинаково  размеченные  потомки  s  APПуть  •  Конечным  путём  σ  системы  переходов  TS  называется  такая  последовательность  чередующихся  состояний  и  действий,  заканчивающаяся  состоянием:  σ = s0a1s1a2 s2 ...an sn , что si ⎯a⎯→ si +1 ∀0 ≤ i < n.i +1•  Бесконечным  путём  σ  системы  переходов  TS  называется  такая  бесконечная  последовательность  чередующихся  состояний  и  действий:  σ = s0a1s1a2 s2a3..., что si ⎯a⎯→ si +1 ∀0 ≤ i.i +1•  Путь  называется  начальным,  если     s0 ∈ IВычисление  •  Путь  называется  максимальным,  если  он  бесконечен.