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

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

0 голосов
/ 30 мая 2018

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

enter image description here

Утверждается, что:

Задача проверки модели для 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 ". </p>

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

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

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

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

1 Ответ

0 голосов
/ 31 мая 2018

Я думаю, что ваш вопрос состоит из двух частей: 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 в одном символическом состоянии.

...