Как исследование символического состояния работает в проверке символьной модели

Question

Следующий алгоритм представляет собой грубый эскиз проверки модели с помощью Computational Tree Logic (CTL):

Заявлено, что:

Задача проверки модели для CTL состоит в том, чтобы проверить для заданной системы переходов TS и формулы CTL Φ, если TS |= Φ... Основная процедура проверки модели CTL довольно проста:

• множество Sat(Φ) всех состояний, удовлетворяющих Φ, вычисляется рекурсивно, и
• отсюда следует, что TS | = Φ тогда и только тогда, когда I ⊆ Sat(Φ), где I - множество начальных состояний TS...

Рекурсивное вычисление Sat(Φ) в основном сводится к обходу снизу вверх дерева разбора формулы состояния CTL Φ.

Таким образом, вы, по сути (насколько я понимаю), вы предоставляете системе формулу CTL Φ, которая является деревом разбора, а затем она просматривает состояния и дерево синтаксического анализа CTL и проверяет, удовлетворяет ли любое состояние Φ.

Вопрос в том:

В методе Sat(Φ) примерно то, что происходит (символический материал). Они говорят (2) ниже, где S - это состояния, а A - атомные суждения. Интересно, как они на самом деле проверяют состояния, учитывая, что программа на самом деле не работает. Это (по крайней мере, я думаю) Проверка символической модели. Хотите знать, можно ли примерно объяснить, как работает проверка состояния? Кажется, что должна произойти какая-то генерация ввода, но в то же время я думаю, что, возможно, этого не произойдет.

Причина, по которой мне трудно это понять, заключается в следующем. Скажем, одно из утверждений для функции addTricky(x, y) который реализован так:

function addTricky(x, y) {
  if (y >= 1) return 3
  return x + y
}

Тогда у меня было бы логическое выражение в некоторой логике, которое говорит: "перед addTricky: z = 0. после z = addTricky(x, y): y >= 1 -> z = 3; y < 1; z = x + y",

В основном пытаюсь добраться до вопроса о моделях. Если Sat(Φ) делает в основном то, что я только что сделал в этом булевом выражении, мне интересно, вызывает ли он когда-либо функцию addTrickyили если он может сделать все это как-то символически. Я пока не понимаю, как это работает, задаюсь вопросом, можно ли немного объяснить основы того, как работает символическое исполнение. Для меня я продолжаю воображать, что это делает своего рода модульное тестирование, например, подключение к сети addTricky(1, 1) например, и проверяя все возможности. Может быть, это "явное исследование состояния" или символическое исследование, не уверен.

Большое спасибо за помощь!

---

(1) Для каждого узла дерева разбора, т. Е. Для каждой подформулы Ψ в Φ, вычисляется множество состояний Sat(Ψ), для которых выполняется Ψ.

(2) Sat(a) = {s ∈ S | a ∈ L(s)}, for any a ∈ A

Answer 1

Я думаю, что ваш вопрос состоит из двух частей: 1) как перейти от функции программного обеспечения к системе перехода и 2) как система перехода используется для проверки удовлетворенности.

1) Система переходов в основном является расширением конечного автомата. Если у вас есть функция, как вы описали, вам сначала нужно преобразовать ее в систему перехода. Это может быть сделано, например, путем введения состояний для каждой исполняемой строки вашего кода и переходов между этими состояниями, которые соответствуют условиям вашего кода. На уровне системы перехода у вас нет концепции вызова функции, поэтому вы должны позаботиться об этом во время перевода, например, путем определения определений функций. Этот шаг не зависит от того, как вы проверяете систему перехода. Как вы можете себе представить, это может привести к довольно большим переходным системам.

Существуют и другие подходы, не основанные на переходных системах, которые имитируют выполнение программы и собирают символические ограничения на этом пути. Символическое исполнение является таким примером.

2) Допустим, вы встроили свою функцию addTricky и получили что-то вроде этого

L0: z=0
    if (y>=1)
L1:     z=3
    else
L2:     z=x+y

Возможный TS это:

(L0: z=0) --[y >= 1]--> (L1: z=3) 
    |
  [y<1]
   \/
(L2: z=x+y)

У вас есть 3 исполняемых оператора, и это приводит к TS с символическими состояниями (S):

 L0: Z=0; X=?; Y=?
 L1: Z=3; X=?; Y>=1
 L2: Z=X+Y; X=?; Y<1

где? означает любое значение. Сила этого подхода заключается в том, что вы можете компактно представить все значения X и Y в одном символическом состоянии.