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

Верификация программ намоделяхЛекция № 10Алгоритмы верификации моделей всистеме SpinИгорь КонновПлан лекции●●Определения из предыдущих лекцийАлгоритм верификации модели для логикилинейного времени●Реализация: поиск в...●Сложность●Подводные камни●Сокращение времени перебора ипотребляемой памяти2Автомат Бюхи●B = (S, s0, L, F, T){или B = (§, Q, ±, q0, F), § = L, Q = S, q0 = s0, ± = T }●Автомат над бесконечными словами!®s1s0´°¯3Автомат Бюхи по формуле LTLB = (S, s0, L, F, T){или B = (§, Q, ±, q0, F), § = L, Q = S, q0 = s0, ± = T }p{p}, {p, r}trues1s0{r}, {p, r}!p || r{r}, {p, r}r{p},{r},{p, r}4[](p -> <> r)Как построить автомат?●●●Формула LTL φРазмер автомата |Bφ| = O(2k), k – числоподформул в формуле φНесколько алгоритмов:–Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper.Simple on-the-fly automatic verification of linear temporallogic.

Proc. PSTV 1995.Реализован в Spin.P. Gastin and D. Oddoux. Fast LTL to Büchi AutomataTranslation. In Proceedings of the 13th InternationalConference on Computer Aided Verification (CAV'01),Paris, France, July 2001, LNCS 2102, pages 53-65.Springer.●–●http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php5Размеченные системыпереходов (LTS)●TS = (S, Act, →a, s0, AP, L)●Act – множество действий, τ ∈ Act●→a ∈ S £ Act £ S – тотальное отношениепереходов●s0 ∈ S – начальное состояние●AP – множество атомарных высказываний●L: S → 2AP – функция разметки6LTS и автоматы Бюхи●Спецификация задаётся автоматом Бюхи●Как сравнить модель (LTS) и автомат Бюхи?●Построить автомат Бюхи по LTS{p, r}{p, r}{p}as0inits1{p}q0q1bc{r}7{p, r}s1{r}Не интересны (структура Крипке)q2Проверка выполнимости●Формула LTL φ и соответствующий автоматБюхи Bφ●LTS M и соответствующий автомат Бюхи BM●Проверить L(BM) = L(Bφ)●БесконечноечисловычисленийПеребрать все вычисления?{p,r}{p}{r}{p,r}...{p,r}{p}{r}{p,r}...8Верификация программы намоделиДолжнобытьпусто!Возможное поведение9Корректное поведениеНекорректноеПроверка на пустоту●Вместо L(BM) = L(Bφ) можно проверить:– L(B ) ∩ L(Bφ) = ∅MЗадачиразрешимы!Надо уметь строить пересечение языков– Надо уметь проверять язык на пустотуМожно проверить:–●– L(B ⊗ Bφ) = ∅M–Так и делает Spin!10Синхронная композиция●Сложно ли построить BM ⊗ Bφ?{p, r}init{p}q0q1{p}{r}{p, r}s1s0q2{p}, {r},{p, r}{p}11Синхронная композиция (2){p, r}init{p}q0{p}, {r}, {p, r}q1{r}{p, r}q2s1s0{r}, {p, r}{r}, {p, r}{p},{r},{p, r}12Синхронная композиция (2){p, r}init{p}q0{p}, {r}, {p, r}q1{r}{p, r}{r}, {p, r}q2s1s0{r}, {p, r}Слово из L(BM ⊗Bφ){p,r}{p}{r}{p},{r},{p, r}13{p,r}{p}Контрпример!...Промежуточные выводы●●Строим L(BM) ∩ L(Bφ) и проверяем напустотуКак видно из предыдущего примера, совсемнеобязательно строить полное пересечение●Достаточно найти одно вычисление●...или убедиться, что нет ни одного вычисления14Поиск в...

глубину●●●●Как найти бесконечное вычислениеконтрпример или убедиться в том, что егонет?Автоматы BM и Bφ конечныДостаточно найти достижимый цикл,содержащий допускающее состояние!Двойной поиск в глубину:–Первый уровень ищет допускающее состояние15–Второй уровень ищет цикл из заданногодопускающего состоянияДвойной поиск в глубину16Организация поискаЗаносим в множество visited(хэш-таблица)Заносим в множество nvisited(или помечаем состояниев хэш-таблице флагом)Проверяем состоянияв стеке поиска первогоуровня17Алгоритм проверки пустотыprocedure emptiness  for all q0 in Q0 do    dfs1(q0);  terminate(false);end procedure18Внешний поискprocedure dfs1(q) var q'; hash_insert(q); // добавить q в visited for all q' in successors(q) do // q -> q'  if not hash_find(q')   dfs1(q'); if is_accepting(q)   dfs2(q);end procedure19Вложенный поискprocedure dfs2(q) var q'; flag(q); // пометить сост.

q в хэш-таблице for all q' in successors(q) do // q -> q'  if q' in dfs1_stack   terminate(true); // обнаружен цикл  else if not has_flag(q')   dfs2(q');end procedure20Почему же алгоритм работает?q0q1...qk ...●qm●Путь q0→q1→...→qk→...→qm→...→qk→...→qk→...принадлежит языкуL(BM ⊗ Bφ)Если цикл черездопускающее состояниенайден, то контрпримерпостроен.21Можно ли пропустить цикл?q0●●Можно ли пропуститьцикл, попав в состояние,помеченное ранее dfs2?Рассмотрим первыйпропущенный цикл.22...Вариантыq0q0qq'qrq'r23Вариант 1Вариант 2Вариантыq0q0Процедура dfs2 должна бытьзапущена сначала из q,а потом из q'qqrq'q'Цикл q'→...→r24→...→q→...пропущен раньшеВариант 1rВариант 2Корректность алгоритмаТеорема (Корректность).

Алгоритм двойногопоиска в глубину строит контрпример длязадачи пустоты автомата Бюхи B тогда и толькотогда, когда L(B) не пусто.25Сложность проверки●●Сложность: O(n1 * n2), где n1, n2 – числосостояний в автоматах BM и Bφ.То есть сложность проверки формулы LTL наLTS M оценивается как O((m+n) * 2k), где m и n– число переходов и состояний в M, а k – числоподформул в φ.26Подводные камни●Не все так просто.●Операции с множествами:●–Вставка в visited, nvisited и stack–Проверка на принадлежность visited, nvisited иstackВ оценке предполагается, что вставка ипроверка на принадлежность занимает O(1).27Ресурсы: время и память●●●Храним visited и stack в хэш-таблицах(nvisited – дополнительный флаг)Операции O(1), но быстро заканчиваетсяпамятьРешение 1: сжатие структур,представляющих состояние (-DCOLLAPSE)––Режим упаковки вектора состояний;коэффициент сжатия от 80% до 90%28Всё равно может довольно быстро закончитьсяпамятьРесурсы: время и память (2)●Решение 2: хэш-таблица фиксированногоразмера с несколькими хэш-функциями(-DHC) (HASHCOMPACT):–Режим упаковки вектора состояний;отображает вектор состояний на число из32+16 бит и сохраняется состояние в хэштаблице (Wolper's hash-compact method).–Рано или поздно, придётся разрешатьколлизии.29Ресурсы: время и память (3)●Решение 3: множества представляютсябитовой шкалой без разрешения коллизий(-DBITSTATE):–Вместо полного перебора используютсяалгоритмы supertrace/bitstate.–Коллизии не разрешаются.

Состояниесчитается просмотренным, если повычисленному хэш-ключу установлен бит.–Аппроксимация!–Можно потерять вычисления.–Вычисляется оценка покрытия.30Другие способыпредставления множеств●●Если не хватает памяти:–можно пожертвовать временем,–не можем ждать годами,–нужен компромисс между потреблениемвремени и памяти.Об этом на следующей лекции...31Почему нужно так многоресурсов?●Большие векторы состояний●Комбинаторный взрыв:– необходиморассмотретьвсевозможные варианты поведенияразличных процессов– Всегда ли это необходимо?32Перебор состоянийПроцесс 1®Процесс 2®¯ИЛИ?¯Процесс 2®¯Процесс 133Перебор состоянийВ спецификацияхне учитывается порядокxиyПроцесс 1x=2Процесс 2x=2y=3ИЛИ?y=3Процесс 2x=2Процесс 1y=334Такой приём не всегдакорректно работаетКаналы c и d пустыПроцесс 1c?xТупикПроцесс 2c?xd!yИЛИ?d!yПроцесс 2c?xПроцесс 1d!y35Редукция частичных порядков●●●На множестве состояний композицииопределяется частичный порядок ⪯.Если s2 ⪯ s1, то переход s1 → s2 можнопропустить при просмотре.Доказывается, что порядок ⪯ сохраняетвыполнимость (и не выполнимость)спецификации.●Запрещается флагом -DNOREDUCE.●Как выбрать порядок ⪯? Эвристика.36Зависимостиx=1x=1y=1y=1x=1g=g+2g=g+2g=g+2g=g*2y=1Только два оператора зависят поданным: g = g + 2 и g = g * 2Остальные операторы независимыпо данным!G.

Holzmann, Cheng Hu. Caltech 2009, CS 118g=g*2y=1g=g*2x=1g=g*2g=g+237Зависимость по данным иуправлениюx=1x=1y=1x=1y=1g=g+2g=g+2g=g*2g=g*2y=1IControlIControlIg=g+2IIControlg=g*2IControlDataData38I – независимые операторыControl – зависимость по управлениюData – зависимость по даннымG. Holzmann, Cheng Hu. Caltech 2009, CS 118Использование зависимостейдля редукцииx=1y=1Независимые операторы:x =1 и y = 1x=1иg=g*2y=1иg=g+2y=1g=g+2g=g+2y=1g=g*2g=g*2x=1g=g*2G.

Holzmann, Cheng Hu. Caltech 2009, CS 118x=1g=g+239Наблюдаемые переменныеx=1y=1[] (x >= y)g=g+2y=1g=g*2x=1g=g+2g=g*2y=1x=1g=g*2G. Holzmann, Cheng Hu. Caltech 2009, CS 118g=g+2Необходимо также учитывать40зависимость по наблюдаемымпеременным (visibility)!Редукцияx=1g=g+2y=1y=1g=g*2x=1x=1 y=1g=g+2g=g+2g=g*2ControlIIControlg=g*2y=1x=1x=1y=1g=g*2g=g+2g=g+2g=g*2G. Holzmann, Cheng Hu.

Caltech 2009, CS 118PPControlII ControlDataData41Правила редукцииПереходы t1 и t2 независимы в состоянии s:–t1 ∈ enabled(s) и t2 ∈ enabled(s)–t1 ∈ enabled(t2(s)) и t2 ∈ enabled(t1(s))Нет зависимости по данным и наблюдаемымсвойствам–Сильная независимость: переходы t1 и t2 сильнонезависимы, если они независимы в любомсостоянии s: t1 ∈ enabled(s) и t2 ∈ enabled(s)●42G. Holzmann, Cheng Hu. Caltech 2009, CS 118Правила редукции (2)Безопасные переходы:●●Переход t1 безопасен, если он независимот всех других переходов системы(правило 1)Оператор i условно безопасен для условияc, если он безопасен во всех состояниях, вкоторых выполняется условие c (правило 2)43СимуляцияКак формально обосновать корректностьредукции?●Обычно для обоснования правил редукциииспользуются отношения симуляции●44Сильная симуляцияM1 = (S1, Act, →1, s01, AP, L1)M2 =(S2, Act, →2, s02, AP, L2)Отношение H ∈ S1 x S2 называетсясимуляцией, если для любых (s1, s2) ∈ H:для любого (s1, a, u1) ∈ →1, то найдётся такойпереход (s2, a, u2) ∈ →1, в котором (u1, u2) ∈ HM1 ⪯ M2, если найдётся H: (s01, s02) ∈ H45Сильная симуляция (пример)®®¯¯¯®46Свойства сильной симуляцииЕсли M1 ⪯ M2 и на M2 выполняется φ из ACTL* (вчастности LTL!), то на M1 также выполняется φ.Строгое соответствие переходов:ττ®®47Слабая симуляцияτττ®®Теряются свойства, не инвариантные кпрореживанию(LTL: оператор neXt).48Спасибо за внимание!При подготовке лекции использовались идеи из курсовлекций Дж.

Хольцмана и Ю.Г. Карпова49.