Главная » Все файлы » Просмотр файлов из архивов » PDF-файлы » Лекция 3. Системы переходов (LTS). Корректность и адекватность LTS модели

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

Описание файла

Файл "Лекция 3. Системы переходов (LTS). Корректность и адекватность LTS модели" внутри архива находится в папке "К. Савенков - Верификация программ на моделях (2012)". PDF-файл из архива "К. Савенков - Верификация программ на моделях (2012)", который расположен в категории "лекции и семинары". Всё это находится в предмете "надёжность программного обеспечения" из седьмого семестра, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст 2 страницы из PDF

 •  Вычислением  системы  переходов  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  –  нет.

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

Свежие статьи
Популярно сейчас