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

Верификация программ намоделяхЛекция № 11Символьные алгоритмы,хранение множеств состоянийИгорь КонновПлан лекцииПростой алгоритм поиска достижимыхсостояний (идея символьных алгоритмов).●●Символьный алгоритм верификации модели.●Двоичные разрешающие диаграммы (BDD).Хранение множеств состояний в Spin:●●BDD,●MDFA.Символьные алгоритмыПоиск достижимых состоянийМожно осуществлять снова поиском вглубину.●●А можно операциями над множествами!●M = (S, Act, →a, s0, AP, L).●Для X ⊆ S обозначим Succ(X) = { t | найдутсятакие s ∈ S и a ∈ Act , что (s, a, t) ∈ → }.Символьный алгоритм поискадостижимых состоянийReach := {s0}; T := ∅;while Reach != T {T := Reach;Reach := Reach ∪ Succ(Reach);}Символьные алгоритмыВместо перебора состояний по отдельностииспользуются операции над множествами.●На этой идее основан целый класссимвольных алгоритмов верификациимоделей (для CTL, LTL и других логик).●Почему (интуитивно понятная) идея поискадостижимых состояний работает?●Как эффективно реализовать операции надмножествами?●Почему это работает?●TS = (S, Act, →a, s0, AP, L).●Множество S конечно.●На множестве 2S задано отношениепорядка ⊆ (т.е.

(2S, ⊆) – решётка):●наименьший элемент – ∅,●наибольший элемент – S.Оператор T: 2S → 2S называетсяпреобразователем предикатов.●Свойства преобразователя●●●●Оператор T – монотонный, если из P ⊆ Qследует T(P) ⊆ T(Q).Оператор T – ∪-непрерывный, если изцепочки P1⊆P2⊆ ...

следует T(∪i Pi) = ∪i T(Pi).Оператор T – ∩-непрерывный, если изцепочки P1 ⊇ P2 ⊇ ... следует T(∩i Pi) = ∩i T(Pi).Пусть задано множество Z ⊆ 2S:–T0(Z) = Z,–Ti+1(Z) = T(Ti(Z)).Следствия теоремы Тарского●●●●Множество X∈ 2S – неподвижная точка,если T(X) = X.У монотонного преобразователя T на 2Sесть наибольшая неподвижная точка¹Z.T(Z)=∩{Z | T(Z)⊆Z} и наименьшаянеподвижная точка ºZ.T(Z)=∪{Z | T(Z)⊇Z}.Для ∩-непрерывного преобразователяверно ¹Z.T(Z)=∪i Ti(∅).Для ∪-непрерывного преобразователяверно ºZ.T(Z)=∩i Ti(S).Леммы для систем переходовЛемма 1. Если S – конечное множество, а T –монотонный преобразователь на конечнойсистеме переходов, то T также ∩непрерывен и ∪-непрерывен.Лемма 2.

Если T – монотонныйпреобразователь, то для любогонатурального числа i имеют местовключения: Ti(∅) ⊆ Ti+1(∅) и Ti(S) ⊇ Ti+1(S).Леммы для систем переходовЛемма 3. Если T – монотонныйпреобразователь, а S – конечное множество,то существуют такие натуральные числа m иn, что для любых i ≥ m и j ≥ n верно: Ti(∅) =Tm(∅) и Tj(S)=Tn(S).Лемма 4. Если T – монотонныйпреобразователь, а S – конечное множество,то существуют такие натуральные числа m иn, что ¹Z.T(Z)=Tm(∅) и ºZ.T(Z)=Tn(S).Вычисление неподвижной точкиQ := ∅; Q' := T(Q);while Q != Q' {Q := Q';Q' := T(Q');}//post: Q – неподвижная точкаДвоичные разрешающиедиаграммы (BDD)Двоичные разрешающиедиаграммы (BDD)С помощью BDD задают булевы функции отn переменных f(x1, ..., xn).●●Ориентированный ациклический граф:–выделены две завершающие вершины: 0 и 1.–Из каждой вершины u (кроме 0 и 1) выходят дведуги low(u) и high(u).–Каждая вершина u помечена переменной var(u).Пример BDDhttp://en.wikipedia.org/wiki/Binary_decision_diagramROBDDНа каждом пути порядок следованияпеременных фиксирован: x1 ≺ x2 ≺ ...

≺ xn●Если var(u) = var(v), low(u) = low(v), high(u) =high(v), то u =v.●Для каждой вершины u верно low(u) !=high(u).●●Каноническое представление, т.е.–Если f(x1, ..., xn) ≡ g(x1, ..., xn), то BDD для fи g совпадают.Иллюстрации правил редукции⇒⇒Правило 1Правило 2ПримерБулева функция для(x1 ↔ y1) ∧ (x2 ↔ y2)Порядок: x1 ≺ x2 ≺ y1 ≺ y2Henrik Reif Andersen.

An Introduction to BinaryDecision DiagramsЕщё примерHenrik Reif Andersen. An Introduction to BinaryDecision DiagramsОперация ограничения●●Пусть задана функция f(x1, ..., xn) и еёROBDD B1.Как построить ROBDD f[xj ← b], т.е. f(x1, ...,xj{1, b, xj+1, ..., xn)?⇒+ редукция!b=0b=1Реализация булевых функций●Разложение Шеннона:–f = (: x ∧ f[x ← 0]) ∨ (x ∧ f[x ← 1]).●Пусть ¤ обозначает ∨, ∧ или :.●Посмотрим, как построить f1 ¤ f2.●●Пусть v и v' – корневые вершины ROBDDдля f1 и f2.x = var(v) и x' = var(v').Варианты 1, 21. Если v и v' – терминальные вершины(0 или 1), то f1 ¤ f2 = value(v) ¤ value(v'),2.

Если x = x', тоf1 ¤ f2=(: x ∧ (f1[x ← 0]¤f2[x ← 0]))∨(x ∧ (f1[x ← 1]¤f2[x ← 1])).Поэтому построим ROBDD u1→(f1[x ← 0]¤f2[x ← 0])и u2→(f1[x ← 1]¤f2[x ← 1]) и создадим вершинуw: var(w) = x, low(w) = u1, high(w) = u2.Варианты 3, 43. Если x < x', то f2[x ← 0] = f2[x ← 1] = f2 иf1 ¤ f2=(: x ∧ (f1[x ← 0]¤f2))∨(x ∧ (f1[x ← 1]¤f2)).Далее, аналогично варианту 2.4. Если x' < x, то аналогично варианту 3.Операция apply●Мы описали операцию apply:–●●На каждом шаге рекурсивно строится BDD дляфункций в разложении ШеннонаДля предотвращения экспоненциальногороста используется кэш (g1 , g2 , ¤) дляфункций, вычисляемых в процессепостроения.Для удаления неиспользуемых вершиниспользуется сборщик мусора.Что же хорошего в BDD?●На BDD определяются операции ∧, ∨ и ¬.Их сложность равна O(m*n), где m и n –число вершин в BDD.●Есть операторы проекции и кванторсуществования:●f(x, 0, 1, z){сложность O(m)}– ∃ y (f(x, y, z)) {сложность O(m*m)}–Как представить нашимножества в виде BDD?●Множество S, |S| = n.

Выберем k: n ≤ 2k–Состояние s ∈ S кодируется с помощьюпеременных x1, ..., xk.–Множество кодируется с помощью булевой функцииf(x1, ..., xk).Отношение переходов кодируется с помощьюбулевой функции T(x1, ..., xk, x'1, ..., x'k).●Применение символьныхалгоритмов и BDD●Для логики ветвящегося времени CTLсимвольные алгоритмы (с BDD) применяютсядля проверки формулы табличным методом:–●Для LTL также применимы символьныеалгоритмы с BDD:–●Верификатор моделей SMV (МакМиллан).Задачу верификации LTL можно свести к задачепроверки CTL с ограничениями справедливости.Э. Кларк мл., О. Грамберг, Д.

Пелед. Верификация моделей программ: Model Checking.Издательство Московского центра непрерывного математического образования. -- М. 2002Символьное представлениемножеств состояний в SpinSpin и BDDBDD можно применять для хранения visited,nvisited и stack.●В Spin используется другое представление:k-уровневый минимизированный конечныйавтомат.●●Состояние кодируется с помощью k словнад алфавитом § = {0, 1, ..., 255}.Автомат, соответствующий множеству,попадает в допускающее состояние на слове⇔ слово соответствует элементу,принадлежащему множеству.●Минимизированый ДКА●Автомат A = ({Qi}ki=0, ±, §).●В автомате k + 1 слой.●Q0 = {q0}, Qk = {0, 1},●±: Qi £ § → Qi+1, 0 ≤ i ≤ k - 1 .●Qi ∩ Qj = ∅ для i ≠ j.●Автомат – минимизированный, т.е.:–L(qi) = L(qj) ⟺ qi = qj.ПримерG.

Holzmann, A. Puri. A Minimized AutomatonRepresentation of Reachable States. InternationalJournal on Software Tools for TechnologyTransfer (STTT), 1999, vol. 2(3), P. 270-278.Операции●●●Проверка вхождения слова в языкавтомата (состояния в множествосостояний): O(k).Добавление слова в автомат сминимизацией: O(k ⋅ |§|).Можно использовать вместо меток нарёбрах метки с диапазонами [i, j] –существенно сокращает размер автоматана практике.Реализация в Spin●Режим использования минимизированногоДКА включается опцией -DMA=n, где:–n – максимальное число байтов (слоёв) вавтомате.Спасибо за внимание!.