lect11 (1158552)
Текст из файла
Верификация программ намоделяхЛекция № 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 – максимальное число байтов (слоёв) вавтомате.Спасибо за внимание!.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.