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

Верификация программна моделяхЛекция №3Системы переходов (LTS). Корректность иадекватность LTS модели.Константин Савенков (лектор)План лекции•••••••Система понятий, используемых в курсеРазмеченные системы переходов (LTS)Недетерминизм систем переходовПути, вычисления, трассыСвойства линейного времениКорректность моделиАдекватность моделиИтоги прошлой лекции• Свойства проверяются на состояниях иих последовательностях• Чтобы перебирать меньше состояний,исследуется не исходная система, а еёмодель• Модель должна быть простой,корректной и адекватной• В этом случае из правильности моделиследует правильность программыСтрого говоря…Если мы хотим доказать, что послепроверки правильности на модели впрограмме нет ошибок, то все эти понятиястоит сформулировать более строгоСтрого говоря, всё должно быть так:Система(программа)(описание)корректнаМодель(описание)Система(системапереходов)корректнаМодель(системапереходов)Система(трассы)корректнаМодель(трассы)адекватнаадекватнаТребованияСвойствалинейноговремениРазличные представленияпрограммыt t lt l ll t lltintmain(){printf(}Исходный кодпрограммыВзлетает,непадает,приземляетсяТребованияГраф программы(ACFG)□(TAKEOFF→(!FALL)U(LANDED))РазмеченнаясистемапереходовlllМножествовычисленийl l tt t ll ll lСпецификацияДопустимые(линейного времени) последовательностиатомарных высказыванийМножествотрассl=Tt=TtltЯзыкдопустимых трассРазмеченные системы переходов (LTS)TS  S , Act , , I , AP, La• S – множество состояний,• Act – множество действий, τ – невидимое действие,a•   S  Act  S – тотальное отношениепереходов,• I  S – множество начальных состояний,• AP – множество атомарных высказываний,• L : S  2 AP – функция разметки.SAct – конечноеaa0s, a0 , s'   s s'– конечное или счётное множество,Нотация:Пример LTS0,?,?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,0x > 02,1,1x -= 1;3,2,03,1,1y += 1;y += 1;Состояние: (счётчик, x, y)x > 04,2,14,1,2x -= 1;2,0,2!(x > 0)5,0,2Пример LTS0,?,?0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:Sint x = 2;1,2,?aint y = 0;2,2,0x > 02,1,1x -= 1;3,2,0x > 03,1,1y += 1;y += 1;Состояние: (счётчик, x, y)S  Act  S4,2,14,1,2x -= 1;I SL2,0,2!(x > 0)5,0,2cnt  0, cnt  1,...

AP   x  0, x  1,...  y  0, y  1,... Что включать в состояние• Набор атомарных высказываний APопределяется свойствами, которые нужнопроверить• Изменение состояния связано с изменениемвыполнимости хотя бы одного атомарноговысказывания• Исходя из этого мы определяем, что включатьв состояние программы• Главное – не «потерять» ни одного измененияатомарных состоянийПример LTS0,?,?0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:Sint x = 2;1,2,?aint y = 0;2,2,0x > 02,1,1x -= 1;3,2,0x > 03,1,1y += 1;y += 1;Состояние: (счётчик, x, y)S  Act  S4,2,14,1,2x -= 1;I SL2,0,2!(x > 0)5,0,2cnt  0, cnt  1,...

APAP  x  0, x  1,...  y  0, y  1,... Пример LTSx=?0: int x = 2;1: int y = 0;2: while (x>0){3:y += 1;4:x -= 1;}5:Sint x = 2;x=2aint y = 0;x=2x > 0x=1x -= 1;x=2x > 0x=1y += 1;y += 1;Состояние: (счётчик, x, y)S  Act  Sx=2x=1x -= 1;I SLx=0!(x > 0)x=0AP  x  0, x  1,...Пример LTSx=?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=2x -= 1;x=1x -= 1;x=0AP  x  0, x  1,...Что включать в состояние?В дальнейшем мы будем рассматривать«универсальное» определение состояния,достаточное для проверки свойствлинейного времени и локализации ихнарушения в описании программыСовокупность значения счётчиковуправления последовательныхпроцессов и переменных программыПример LTSint 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)Часть состояний не показана(оператор беск.

цикла,стартовые состояния)ProdCons(1.1,2.1),0p < 2p -= 1(1.1,2.1),1(1.2,2.1),0p += 1p > 0(1.1,2.1),1p < 2p -= 1p < 2(1.2,2.1),1p += 1p > 0(1.1,2.1),2p > 0(1.1,2.1),2(1.1,2.1),1p += 1p -= 1Бесконечное количество вычислений, однакоразмеченная система переходов конечнаНедетерминизм• В ряде ситуаций шаг может сделать любойиз двух процессов, порядок действий неопределён• Недетерминизм = неопределённость• При построении LTS рассматриваются всевозможные варианты последовательностидействийНедетерминизм• Вообще-то в природе довольно малонедетерминированных процессов• Да и те считаются недетерминированными,поскольку физические законы, по которымвыбирается действие, нам не известны• Недетерминизм появляется, как только мыне знаем причин выбора действия илисчитаем их несущественнымиНедетерминизм• Порядок выполнения Prod и Cond наконкретном компьютере детерминирован иопределяется алгоритмом диспетчераоперационной системы и состоянием ресурсов• Для проверки правильности программы мырешили абстрагироваться от всего, кромеописания двух процессов• Итог – недетерминизм очерёдностивыполнения процессовПодробнее про разные видынедетерминизма – нижеНедетерминизм – это фича!• Используется для:– моделирования параллельного выполненияпроцессов в режиме чередования(интерливинга)• позволяет абстрагироваться от алгоритмадиспетчеризации и скорости выполнения процессовНедетерминизм – это фича!• Используется для:– моделирования прототипа системы• не ограничивает будущую реализацию заданнымпорядком выполнения операторов иликонкретными входными даннымиНедетерминизм – это фича!• Используется для:– построения абстракции реальной системы• для абстрагирования от деталей, несущественныхдля проверки свойств и для построения модели понеполной информацииНедетерминизм в LTS• В LTS недетерминизм проявляется в видесостояний, из которых можно перейтиболее чем в одно состояниеAP  {a}abaнедетерминизмдействийaнедетерминизматомарных высказыванийстрогие определения – далееНедетерминизм в LTS• В LTS недетерминизм проявляется в видесостояний, из которых можно перейтиболее чем в одно состояние??может произойти одноиз нескольких действийнаблюдатель не можетотличить два состояниястрогие определения – далееВспомогательные определенияПрямые потомки вершины sпо действию aпо всем действиямaPost ( s, a )  {s' S | s s' }, Post ( s )  Post ( s, a )ssa a b ca a b caActПрямые предки вершины sпо действию aпо всем действиямaPre( s, a )  {s' S | s' s}, Pre( s )  Pre( s, a )aActa a b ca a b cssДетерминизм• Система TS  S , Act , , I , AP, Laдетерминирована– по действиям, тогда и только тогда:I 1 иPost ( s, a )  1, s  S , a  Act– по атомарным высказываниям, тогда и толькотогда:I 1 иPost ( s)  s' S | L( s' )  A  1, s  S , A  2 APодинаково размеченные потомки sПуть• Конечным путём σ системы переходов TS называетсятакая последовательность чередующихся состояний идействий, заканчивающаяся состоянием:  s0a1s1a2 s2 ...an sn , что si  si 1 0  i  n.ai 1• Бесконечным путём σ системы переходов TS называетсятакая бесконечная последовательность чередующихсясостояний и действий:  s0a1s1a2 s2a3..., что si a si 1 0  i.i 1• Путь называется начальным, еслиs0  IВычисление• Путь называется максимальным, если онбесконечен.• Вычислением системы переходов TSназывается начальный максимальный путь.Примеры вычислений0,?,?int x = 2;p < 21,2,?x > 02,1,1x -= 1;3,2,0x > 03,1,1y += 1;y += 1;4,2,14,1,2x -= 1;2,0,2!(x > 0)5,0,2p -= 1(1.1,2.1),1(1.2,2.1),0int y = 0;2,2,0(1.1,2.1),0p += 1p > 0(1.1,2.1),1p < 2p -= 1p < 2(1.2,2.1),1p += 1p > 0(1.1,2.1),2p > 0(1.1,2.1),2p -= 1(1.1,2.1),1p += 1Примеры вычислений0,?,?int x = 2;p < 21,2,?x > 02,1,1x -= 1;3,2,0x > 03,1,1y += 1;y += 1;4,2,14,1,2x -= 1;2,0,2!(x > 0)5,0,2p -= 1(1.1,2.1),1(1.2,2.1),0int y = 0;2,2,0(1.1,2.1),0p += 1p > 0(1.1,2.1),1p < 2p -= 1p < 2(1.2,2.1),1p += 1p > 0(1.1,2.1),2p > 0(1.1,2.1),2p -= 1(1.1,2.1),1p += 1Примеры вычислений0,?,?int x = 2;p < 21,2,?x > 02,1,1x -= 1;3,2,0x > 03,1,1y += 1;y += 1;4,2,14,1,2x -= 1;2,0,2!(x > 0)5,0,2p -= 1(1.1,2.1),1(1.2,2.1),0int y = 0;2,2,0(1.1,2.1),0p += 1p > 0(1.1,2.1),1p < 2p -= 1p < 2(1.2,2.1),1p += 1p > 0(1.1,2.1),2p > 0(1.1,2.1),2p -= 1(1.1,2.1),1p += 1Примеры вычислений0,?,?int x = 2;p < 21,2,?x > 02,1,1x -= 1;3,2,0x > 03,1,1y += 1;y += 1;4,2,14,1,2x -= 1;2,0,2!(x > 0)5,0,2p -= 1(1.1,2.1),1(1.2,2.1),0int y = 0;2,2,0(1.1,2.1),0p += 1p > 0(1.1,2.1),1p < 2p -= 1p < 2(1.2,2.1),1p += 1p > 0(1.1,2.1),2p > 0(1.1,2.1),2p -= 1(1.1,2.1),1p += 1Примеры вычислений0,?,?int x = 2;p < 21,2,?x > 02,1,1x -= 1;3,2,0x > 03,1,1y += 1;y += 1;4,2,14,1,2x -= 1;2,0,2!(x > 0)5,0,2p -= 1(1.1,2.1),1(1.2,2.1),0int y = 0;2,2,0(1.1,2.1),0p += 1p > 0(1.1,2.1),1p < 2p -= 1p < 2(1.2,2.1),1p += 1p > 0(1.1,2.1),2p > 0(1.1,2.1),2p -= 1(1.1,2.1),1p += 1Достижимость состояний• Состояние s  S называется достижимым(из начального) в системе переходов TS,если существует начальный, конечный путьs0  s1  ...

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