Этот вопрос касается того, как сгенерировать символическое пространство состояний для средства проверки символьной модели. Сначала я вхожу в предысторию, которая заставляет меня хотеть сделать это для MDD, затем я объясняю вопрос более подробно.
Эта лекция Эдмунда М. Кларка (один основателей Model Checking) представляет проверку символьных моделей. В нем говорится, что средства проверки моделей «промышленной силы» используют логическое кодирование (бинарные диаграммы принятия решений или BDD) для решения проблемы взрыва состояния. Однако он допускает лишь на порядок больше состояний, чем обычная проверка модели. Я пропустил обычную проверку модели, которая напрямую строит граф переходов состояний программы, потому что я могу представить, что это нецелесообразно сразу.
Я видел несколько статей, описывающих лучшие качества, чем BDD, такие как обработка большего количества состояний1 (избегая?! проблемы взрыва пространства состояний), общее ускорение2 (ограниченное проверка модели), используя методы сопоставления состояний для ограничения поиска в пространстве состояний (помимо ограниченной проверки модели)3 и использование MDD, которые работают на несколько порядков быстрее, чем существующие BDD[4][5].
BDD увеличил количество состояний, поддерживаемых на в среднем примерно от 10^6 до 10^20. В этой бумаге также говорится:
К сожалению, известно, что символьные методы плохо работают для асинхронных систем, таких как протоколы связи, которые особенно страдают от взрыва пространства состояний.
Таким образом, кажется, что MDD или даже EDD являются лучшим выбором для проверки модели. Существуют также BDD с краевым значением (EVBDD). Но тогда мой вопрос заключается в том, как построить символическое пространство состояний для ~MDD (или того, что лучше). Этот документ представляет его, но не объяснить, как на самом деле генерировать его. Они заявляют:
Мы используем квазиредуцированные, упорядоченные, неотрицательные краевые многозначные диаграммы решений.
Интересно, можно ли объяснить алгоритм генерации пространства состояний для MDD на высоком уровне и какие структуры данных задействованы в системе, например, каковы свойства объекта node (например, структура C). Я думаю, что если я смогу увидеть общую картину того, что представляют собой структуры данных и примерно как работает алгоритм, этого будет достаточно для реализации.
Кроме того, я не уверен, что нужно сделать с исходной программой и спецификацией. Поэтому, если бы объяснение могло быстро описать/представить, как генерировать любые промежуточные объекты, это было бы полезно. Добавление этого, потому что я видел в одной бумаге, что у них есть программа в форме сети Петри которые они затем преобразуют в MDD, и я не уверен, как преобразовать программу в сеть Петри и нужно ли это вообще. В основном, как перейти от исходного кода к MDD на высоком уровне.
Я думаю, что это изображение является алгоритмом генерации пространства состояний, но мне было трудно понять его детали. В частности, задействованные структуры данных и откуда берется «состояние», то есть являются ли они логическими предикатами из какой-то другой модели или чего-то еще.
Этот тоже кажется близким:
Вот еще из той же газеты:
(1) В этой статье мы показываем, как логические процедуры принятия решений, такие как метод Сталмарка [16 ] или процедуру Дэвиса и Патнэма [7], могут заменить BDD. Этот новый метод позволяет избежать избыточного пространства BDD, гораздо быстрее генерирует контрпримеры, а иногда и ускоряет проверку.
(2) Основным результатом статьи является улучшение O (N) во временной сложности проверки ограниченных во времени до-формул, где N — число состояний в рассматриваемом CTMC.
(3) Мы основываемся на нашей предыдущей работе, в которой мы предложили комбинацию символьного выполнения и проверки моделей для анализа программ со сложными входными данными [14,19]. В этой работе мы ограничиваем размер входных данных и (или) глубину поиска средства проверки модели. Здесь мы выходим за рамки проверки ограниченной модели и изучаем методы сопоставления состояний, чтобы ограничить поиск в пространстве состояний. Мы предлагаем метод проверки того, когда символическое состояние входит в состав другого символьного состояния.
(4) Мы представляем новый алгоритм для генерации пространств состояний асинхронных систем с использованием диаграмм многозначных решений. В отличие от родственных работ, мы кодируем функцию следующего состояния системы не как одну булевую функцию, а как векторное произведение целочисленных функций. Это позволяет применять различные стратегии итерации для построения пространства состояний системы. В частности, мы вводим новую элегантную стратегию, называемую насыщением, и реализуем ее в инструменте SMART. Вдобавок к тому, что он обычно работает на несколько порядков быстрее, чем существующие генераторы пространства состояний на основе BDD, требуемая пиковая память нашего алгоритма часто близка к конечной памяти, необходимой для хранения всего пространства состояний.
(5) Символьные методы на основе двоичного Диаграммы принятия решений (BDD) широко используются для рассуждений о временных свойствах аппаратных схем и синхронных контроллеров. Однако они часто плохо работают при работе с огромными пространствами состояний, лежащими в основе систем, основанных на семантике чередования, таких как протоколы связи и распределенное программное обеспечение, которые состоят из независимо действующих подсистем, взаимодействующих через общие события... В этой статье показано, что эффективность Методы исследования пространства состояний с использованием диаграмм решений могут быть значительно улучшены за счет использования семантики чередования, лежащей в основе многих системных моделей, основанных на событиях и компонентах. Представлен новый алгоритм символьной генерации пространств состояний, который (i) кодирует векторы состояния модели с помощью многозначных диаграмм решений (MDD), а не сглаживает их в BDD.
Знакомство с этим:
Пространство достижимых состояний X_reach можно охарактеризовать как наименьшее решение уравнения фиксированной точки X ⊆ X_init ∪ T(X). Алгоритм
Bfsреализует именно это вычисление с фиксированной точкой, где наборы и отношения хранятся с использованием MDD L-уровня и 2L-уровня соответственно, т. е. узел p кодирует множество X_p, имеющее характеристическую функцию v_p, удовлетворяющуюv_p(i_L,...,i_1) = 1 ⇔ (i_L,...,i_1) ∈ X_p.
Объединение множеств просто реализуется путем применения оператора Or к их характеристическим функциям, а вычисление состояний, достижимых за один шаг, реализуется с помощью функции RelProd (конечно, если используются MDD-версии этих функций, необходимо использовать MDD-версию этих функций). вместо BDD). Поскольку он выполняет символический поиск в ширину, алгоритм Bfs останавливается ровно за столько итераций, сколько максимальное расстояние любого достижимого состояния от начальных состояний.
mdd Bfs(mdd Xinit) is
local mdd p;
p ← Xinit;
repeat
p ← Or(p, RelProd(p, T ));
until p does not change;
return p;
bdd Or(bdd a, bdd b) is
local bdd r, r0, r1;
local level k;
if a = 0 or b = 1 then return b;
if b = 0 or a = 1 then return a;
if a = b then return a;
if Cache contains entry hORcode, {a, b} : ri then return r;
if a.lvl < b.lvl then
k ← b.lvl;
r0 ← Or(a, b[0]);
r1 ← Or(a, b[1]);
else if a.lvl > b.lvl then
k ← a.lvl;
r0 ← Or(a[0], b);
r1 ← Or(a[1], b);
else • a.lvl = b.lvl
k ← a.lvl;
r0 ← Or(a[0], b[0]);
r1 ← Or(a[1], b[1]);
r ← UniqueTableInsert(k, r0, r1);
enter hORcode, {a, b} : ri in Cache;
return r;
bdd RelProd(bdd x, bdd2 t) is • quasi-reduced version
local bdd r, r0, r1;
if x = 0 or t = 0 then return 0;
if x = 1 and t = 1 then return 1;
if Cache contains entry hRELPRODcode, x, t : ri then return r;
r0 ← Or(RelProd(x[0], t[0][0]), RelProd(x[1], t[1][0]));
r1 ← Or(RelProd(x[0], t[0][1]), RelProd(x[1], t[1][1]));
r ← UniqueTableInsert(x.lvl, r0, r1);
enter hRELPRODcode, x, t : ri in Cache;
mdd Saturation(mdd Xinit) is
return Saturate(L, Xinit);
mdd Saturate(level k, mdd p) is
local mdd r, r0, ..., rnk−1;
if p = 0 then return 0;
if p = 1 then return 1;
if Cache contains entry hSATcode, p : ri then return r;
for i = to nk − 1 do
ri ← Saturate(k − 1, p[i]);
repeat
choose e ∈ Ek, i, j ∈ Xk, such that ri 6= 0 and Te[i][j] 6= 0;
rj ← Or(rj , RelProdSat(k − 1, ri, Te[i][j]));
until r0, ..., rnk−1 do not change;
r ← UniqueTableInsert(k, r0, ..., rnk−1);
enter hSATcode, p : ri in Cache;
return r;
mdd RelProdSat(level k, mdd q, mdd2 f) is
local mdd r, r0, ..., rnk−1;
if q = 0 or f = 0 then return 0;
if Cache contains entry hRELPRODSATcode, q, f : ri then return r;
for each i, j ∈ Xk such that q[i] 6= 0 and f[i][j] 6= 0 do
rj ← Or(rj , RelProdSat(k − 1, q[i], f[i][j]));
r ← Saturate(k, UniqueTableInsert(k, r0, ..., rnk−1));
enter hRELPRODSATcode, q, f : ri in Cache;
return r.
