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

 •  Вычислением  системы  переходов  TS  называется  начальный  максимальный  путь.  Примеры  вычислений  0,?,?  int x = 2;1,2,?  x > 03,2,0  x > 03,1,1  y += 1;y += 1;4,2,1  4,1,2  x -= 1;2,0,2  !(x > 0)5,0,2  (1.1,2.2),1  (1.2,2.1),0  2,1,1  x -= 1;p -= 1p < 2int y = 0;2,2,0  (1.1,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  p -= 1(1.2,2.2),1  p += 1Примеры  вычислений  0,?,?  int x = 2;1,2,?  x > 03,2,0  x > 03,1,1  y += 1;y += 1;4,2,1  4,1,2  x -= 1;2,0,2  !(x > 0)5,0,2  (1.1,2.2),1  (1.2,2.1),0  2,1,1  x -= 1;p -= 1p < 2int y = 0;2,2,0  (1.1,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  p -= 1(1.2,2.2),1  p += 1Примеры  вычислений  0,?,?  int x = 2;1,2,?  x > 03,2,0  x > 03,1,1  y += 1;y += 1;4,2,1  4,1,2  x -= 1;2,0,2  !(x > 0)5,0,2  (1.1,2.2),1  (1.2,2.1),0  2,1,1  x -= 1;p -= 1p < 2int y = 0;2,2,0  (1.1,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  p -= 1(1.2,2.2),1  p += 1Примеры  вычислений  0,?,?  int x = 2;1,2,?  x > 03,2,0  x > 03,1,1  y += 1;y += 1;4,2,1  4,1,2  x -= 1;2,0,2  !(x > 0)5,0,2  (1.1,2.2),1  (1.2,2.1),0  2,1,1  x -= 1;p -= 1p < 2int y = 0;2,2,0  (1.1,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  p -= 1(1.2,2.2),1  p += 1Примеры  вычислений  0,?,?  int x = 2;1,2,?  x > 03,2,0  x > 03,1,1  y += 1;y += 1;4,2,1  4,1,2  x -= 1;2,0,2  !(x > 0)5,0,2  (1.1,2.2),1  (1.2,2.1),0  2,1,1  x -= 1;p -= 1p < 2int y = 0;2,2,0  (1.1,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  p -= 1(1.2,2.2),1  p += 1Достижимость  состояний  •  Состояние      s    ∈          S        называется  достижимым  (из  начального)  в  системе  переходов  TS,  если  существует  начальный,  конечный  путь  a1a2ans0 ⎯⎯→ s1 ⎯⎯→ ...

⎯⎯→ sn = s.•  Reach(TS)  обозначает  множество  всех  состояний,  достижимых  в  TS.  Трассы  •  Вычисление  описывает  последовательность  состояний  и  действий;  что  происходит  в  системе.  Требуется  для  описания  семантики  программы  (позже).  •  Свойства  корректности  формулируются  в  терминах  последовательностей  значений  атомарных  высказываний  в  состояниях  модели.  Трассы  •  Система  переходов:  aTS = S , Act, ⎯⎯→, I , AP, L•  Путь  (фрагмент  вычисления):  •  Трасса:  σ = s0a1s1a2 s2a3...AP ωtr = L( s0 ) L( s1 ) L( s2 )...

∈ (2 )фокусируемся  на  «наблюдаемом»  поведении  Примеры  трасс  вычисление  (1.1,2.1),0  трасса  {a ≡ p = 0}a  ⎧a ≡ p ≠ 0⎫трасса  2   ⎨ b ≡ p = 1 ⎬⎩⎭!a   !b  p < 2(1.2,2.1),0  a  !a   !b  !a  a   b  !a  a   b  a  !a   !b  a  !a   !b  p += 1(1.1,2.1),1  p > 0(1.1,2.1),1  p -= 1(1.1,2.1),0  p < 2(1.2,2.1),0  p += 1...Свойства  линейного  времени  •  Атомарные  высказывания:  a  -­‐  «находимся  в  точке  отправки  запроса»    b  -­‐  «находимся  в  точке  приёма  ответа»  •  Свойство:    «после  отправки  запроса  рано  или  поздно  получим  ответ»  •  Пример  допустимых  трасс:  a  Ø  Ø  Ø  Ø  Ø  b  Ø  …  Ø  Ø  Ø  Ø  Ø  Ø  Ø  …  •  Пример  недопустимых  трасс:  a  Ø  Ø  Ø  Ø  Ø  Ø  Ø  …  a  Ø  Ø  Ø  Ø  b  a  Ø  …  Свойства  линейного  времени  •  Свойство  φ  определяет  набор  допустимых  трасс,  AP ωϕ ⊆ (2 )•  Свойство  φ  выполнимо  на  трассе  σ:  σ ϕ ⇔ σ ∈ϕ  •  Система  переходов  TS  удовлетворяет  свойству  линейного  времени  φ:  TS ϕ ⇔ Traces(TS ) ⊆ ϕTS ( P ) ϕ ≡ P ϕСхема  понятий  Система  (описание)  корректна  Модель  (описание)  Система  (система  переходов)  корректна  Модель  (система  переходов)  Система  (трассы)  корректна  Модель  (трассы)  адекватна  адекватна  Требования  Свойства  линейного  времени  Абстракция  трасс  •  Представим  трассу  в  форме  интерпретации  I:  I (tr) = Ν, ≤, ξгде      N          –  множество  натуральных  чисел,                      ≤        –  отношение  порядка  на    N        ,  а                      ξ      :      N        ×        AP              →          {    T,          ⊥      }    ,  и  при  этом  ∀n > 0, p ∈ APξ ( n , p ) = T ⇔ p ∈ L( s )Абстракция  трасс  •  Рассмотрим  трассы  tr  и  tr’  такие,  что:  I (tr) = Ν, ≤, ξI (tr' ) = Ν, ≤, ξ 'ξ : N × AP → {T, ⊥} ξ ' : N × AP' → {T, ⊥}•  Будем  говорить,  что  tr’  является  (корректной)  абстракцией  tr  (  tr                tr      '),  если  AP' ⊆ AP∃α : N → N : ∀n, k ∈ N (n ≤ k ⇒ α (n) ≤ α (k ) )∀n ∈ N , p ∈ AP' (ξ (n, p) = ξ ' (α (n), p) )Пример  абстракции  трасс  p  =  T  q  =  F  r  =  F  p  =  T  q  =  F  r  =  T  p  =  F  q  =  F  r  =  F  p  =  F  q  =  T  r  =  T  p  =  F  q  =  T  r  =  F  AP={p,q,r}  p  =  T  q  =  F  p  =  T  q  =  F  p  =  F  q  =  F  p  =  F  q  =  T  p  =  F  q  =  T  AP’={p,q}  p  =  T  q  =  F  p  =  F  q  =  F  p  =  F  q  =  T  AP’={p,q}  Схема  понятий  Система  (описание)  корректна  Модель  (описание)  Система  (система  переходов)  корректна  Модель  (система  переходов)  Система  (трассы)  корректна  Модель  (трассы)  адекватна  адекватна  Требования  Свойства  линейного  времени  Условие  корректности  модели  •  Пусть  P  –  система,  φ  –  произвольное  свойство  линейного  времени.

 (Корректной)  моделью  P  называется  такое  М,  что:  если  свойство  выполняется  на  модели,  то  оно  выполняется  и  на  системе  •  Это  выполняется  тогда  и  только  тогда,  когда:  для  любой  трассы  исходной  системы  в  модели  найдётся  её  корректная  абстракция  Условие  корректности  модели  •  Пусть  P  –  система,  φ  –  произвольное  свойство  линейного  времени.  (Корректной)  моделью  P  называется  такое  М,  что:  M ϕ⇒P ϕпозволяет  проверять  свойства  программы  на  её  модели  определение  •  Это  выполняется  тогда  и  только  тогда,  когда:  ∀tr ∈ Traces(TS ( P ))∃tr'∈ Traces(TS ( M )) :tr  tr'для  проверки  такого  условия  нужно  рассмотреть  все  трассы  исходной  системы    допускает,  что  в  модели  больше  состояний  необходимое  и  достаточное  условие    Достаточное  условие  корректности  •  Какими  же  свойствами  должна  обладать  TS  модели,  чтобы  быть  корректной?  –  действиям  и  атомарным  высказываниям  модели  должны  быть  сопоставлены  действия  и  атомарные  высказывания  системы,  –  каждому  состоянию  системы  должно  быть  сопоставлено  состояние  модели,  –  модель  должна  корректно  сохранять  множество  начальных  состояний,  –  если  в  системе  есть  переход  между  двумя  состояниями,  в  модели  должен  быть  переход  по  между  соотв.

 состояниями  по  соотв.  действию,  –  соотв.  состояния  в  модели  и  системе  должны  быть  размечены  атомарными  высказываниями  модели  одинаково.  Достаточное  условие  корректности  •  Какими  же  свойствами  должна  обладать  TS  модели,  чтобы  быть  корректной?  aTS = S , Act, ⎯⎯→, I , AP, LaTS ' = S ' , Act' , ⎯⎯→' , I ' , AP' , L'Act ' ⊆ ActAP ' ⊆ AP∃α : S → S ' , s0 ' = α ( s0 )aas1 ⎯⎯→s2 ⇒ α ( s1 ) ⎯⎯→α ( s2 )∀s ∈ S , L' (α ( s )) = L( s ) ∩ AP 'достаточное  условие  Пример  корректной  абстракции  системы  переходов  p  =  T,q  =  T  q  =  T  q  =  T  a  a  p  =  F,q  =  F  a  q  =  F  q  =  F  b  b  p  =  T,q  =  T  b  q  =  T  d  p  =  F,q  =  T  c  d  c  e  q  =  T  f  f  q  =  T  τ  (P)  f  e  q  =  F  p  =  F,q  =  T  e  q  =  F  q  =  T  p  =  T,q  =  F  q  =  T  d  τ  τ  (M1)  (M2)  c  Схема  понятий  Система  (описание)  корректна  Модель  (описание)  Система  (система  переходов)  корректна  Модель  (система  переходов)  Система  (трассы)  корректна  Модель  (трассы)  адекватна  адекватна  Требования  Свойства  линейного  времени  Адекватность  модели  •  Модель  называется  адекватной,  если:  1.  Атомарные  высказывания,  в  терминах  которых  задаются  свойства,  присутствуют  в  разметке  модели  2.  Из  нарушения  свойства  на  модели  следует,  что  оно  нарушается  и  на  исходной  системе  Адекватность  модели  •  Модель  называется  адекватной,  если:  1.     APϕ ⊆ APMнеобходимое  условие  (можно  вычислить)  2.     M ϕ⇒P ϕдостаточное  условие  (нельзя  вычислить)  •  Определить  адекватность  при  построении  нельзя,  можно  лишь  обнаружить  несоответствие  и  исправить  модель  Пример  корректной  абстракции  системы  переходов  p  =  T,q  =  T  q  =  T  q  =  T  a  a  p  =  F,q  =  F  a  q  =  F  q  =  F  b  b  p  =  T,q  =  T  b  q  =  T  d  p  =  F,q  =  T  c  d  c  e  q  =  T  f  f  q  =  T  τ  (P)  f  e  q  =  F  p  =  F,q  =  T  e  q  =  F  q  =  T  p  =  T,q  =  F  q  =  T  d  τ  τ  (M1)  (M2)  c  Пример  –  проверяемые  свойства  •  В  любом  вычислении  встречается  состояние,  когда  p=T∧q=T  –  ни  одна  из  моделей  не  адекватна,  •  Для  любого  пути  верно,  что  за  любым  q=  F  рано  или  поздно  встретится  q=  T  –  все  модели  адекватны,  •  Между  двумя  состояниями  с  q=  F  встречается  не  более  чем  3  состояния  с  q=  T  –  модель  М1  адекватна,  М2  –  нет.

   Схема  понятий  Система  (описание)  корректна  Модель  (описание)  Система  (система  переходов)  корректна  Модель  (система  переходов)  Система  (трассы)  корректна  Модель  (трассы)  адекватна  адекватна  Требования  Свойства  линейного  времени  Спасибо за внимание!Вопросы?.