Этот вопрос о том, как создать символьное пространство состояний для проверки символьной модели.Сначала я подхожу к некоторому фону, который заставляет меня хотеть сделать это для MDD, затем я объясняю вопрос более подробно.
Эта лекция Эдмунда М. Кларка (один из основателей)проверки моделей) вводит символическую проверку моделей.В нем говорится, что в контроллерах моделей "промышленного уровня" используется логическое кодирование (двоичные диаграммы решений, или 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) Мы представляем новый алгоритм генерации пространств состояний асинхронных систем с использованием многозначных диаграмм решений,В отличие от связанной работы, мы кодируем функцию next {state системы не в виде одной булевой функции, а в виде перекрестных {произведений целочисленных функций.Это позволяет применять различные итерационные стратегии для построения пространства состояний системы.В частности, мы вводим новую элегантную стратегию под названием насыщенность и внедряем ее в инструмент SMART.Помимо того, что обычно выполняемые на несколько порядков величины быстрее, чем существующие генераторы пространства состояний на основе BDD, требуемая пиковая память нашего алгоритма часто близка к конечной памяти, необходимой для хранения общего пространства состояний.
(5) Символьные методы, основанные на двоичных диаграммах принятия решений (BDD), широко используются для рассуждения о временных свойствах аппаратных схем и синхронных контроллеров.Однако они часто плохо работают при работе с огромными пространствами состояний, лежащими в основе систем, основанных на семантике чередования, такой как протоколы связи и распределенное программное обеспечение, которые состоят из независимо действующих подсистем, которые обмениваются данными через общие события ... Эта статья показывает, что эффективностьметоды исследования состояния пространства с использованием диаграмм решений могут быть значительно улучшены путем использования семантики чередования, лежащей в основе многих моделей систем, основанных на событиях и компонентах.Представлен новый алгоритм символического генерирования пространств состояний, который (i) кодирует векторы состояния модели с помощью многозначных диаграмм решений (MDD), а не объединяет их в BDD.
Сближение с this :
Достижимое пространство состояний 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 этих функций должна использоваться, если вместо BDD используются MDD).Поскольку он выполняет поиск символа в ширину, алгоритм 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.