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

Следующий алгоритм представляет собой грубый набросок проверки модели. с логикой вычислительного дерева (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 ; г = х + у".

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

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

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

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

logic algorithm formal-verification model-checking
person Lance Pollard    schedule 30.05.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

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

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

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

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

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

Возможный ТС:

(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 в одном символьном состоянии.

person Marco    schedule 31.05.2018