Вельдер С.Э. и др. Верификация автоматных программ

Подождите немного. Документ загружается.

, z

Рис. 2.13. Таблица для формулы G(z

 (z

W z

))

Таким образом, в наличии все переходы:

 между состояниями левого и среднего блоков;

 между состояниями среднего и правого блоков;

 из состояний левого блока в состояния правого;

 между верхним состоянием и средним блоком;

 из состояний левого блока в верхнее состояние;

 из верхнего состояния в состояния правого блока.

Никаких других переходов нет (в частности, нет перехода из верхнего

состояния в себя).

Проверка моделей

Через L

(M) обозначим множество (бесконечных) путей модели M.

Оно называется языком модели. Таблица, соответствующая формуле

φ, обозначается T

. Имея такой ключевой результат, как построение

таблиц, можно описать базовую схему проверки моделей для LTL-

формул.

Наивный метод проверки, выполняется ли LTL-формула φ для

заданной модели M, состоит в следующем: построим таблицу T

для

формулы φ, а после этого проверим, верно ли L

(M)  L

Допускающие вычисления системы M соответствуют возможному

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

соответствуют желаемому поведению модели. Если любое

возможное поведение является желаемым (если L

(M)  L

)), то

можно заключить, что модель удовлетворяет формуле φ. Данный

подход кажется приемлемым. Однако задача проверки включения

языков для моделей Крипке PSPACE-полна относительно своих

входных данных. Это затрудняет проверку моделей таким методом.

Заметим, что L

(M)  L

)  (L

(M)  L

(T

) = ), где T

(это

дополнение T

) – такая модель, множеством путей которой является

дополнение множества путей T

. Однако, наилучший известный

алгоритм построения T

по таблице T

квадратично экспоненциален:

если T

содержит n состояний, то T

содержит c

состояний для

некоторой константы c > 1. Это означает, что результирующая модель

очень велика.

Используя свойство, состоящее в том, что дополняющая модель для T

эквивалентна модели для отрицания φ (L

(T

) = L

φ

)), получим

следующий более эффективный метод проверки моделей LTL. Его

идея состоит в том, чтобы построить таблицу для отрицания

желаемого свойства φ. Таким образом, таблица T

φ

моделирует

нежелательные вычисления системы, которую требуется проверить.

Если M содержит определенный допускающий путь, который также

является допускающим путем T

φ

, то это пример вычисления, которое

нарушает свойство φ. В этом случае можно сделать вывод о том, что φ

не является свойством модели M. Если же нет такого общего

вычисления, то φ выполняется. Это объясняет последний шаг

следующего метода: построить таблицу T

для формулы φ и после

этого проверить, верно ли L

(M)  L

φ

) = .

Для проверки последнего равенства строится декартово произведение

моделей M и T

φ

. Пусть модель M имеет вид (S, R, S

, Label), а модель

φ

представляет собой четверку (S

, R

, S

, Label

), где S

–

множество стартовых состояний, которых может быть несколько.

Тогда модель-произведение M' = (S', R', S

', Label') строится

следующим образом:

S' = {(s, s

) | s  S, s

 S

и Label

)  AP = Label(q)};

R' = {((s, s

), (s', s

')) | (s, s')  R, (s

, s

')  R

}  (S' × S');

' = {(s

, s

) | s

 S

, s

 S

}  S';

Label'(s, s

) = Label

Определим условия справедливости t

для данной системы и

проверим, существует ли в модели M' бесконечный путь, стартующий

из начального состояния и удовлетворяющий условиям

справедливости (эффективный алгоритм, решающий эту задачу,

обсуждается в разд. 2.4). Если такой путь существует, то в M

существует путь, удовлетворяющий φ. Этот путь является

контрпримером для формулы φ.

Временная сложность данного алгоритма O(|S| × 2

|φ|

). Отметим, что

задача проверки моделей для LTL является PSPACE-полной – для ее

решения требуется размер памяти как минимум полиномиальный

относительно размера входных данных [25].

2.2.7. Верификация LTL при помощи автоматов Бюхи

При проверке LTL-свойств могут использоваться различные способы

представления LTL-формулы в виде графа переходов. Один из таких

способов был рассмотрен в предыдущем разделе. Еще один, похожий

способ, использует так называемые автоматы Бюхи.

Пусть AP – множество атомарных предложений. Автоматом Бюхи

над алфавитом 2

называется четверка A = (Q, q



, F), где

 Q – конечное множество состояний;

 q

– начальное состояние;





 Q  2

 Q – тотальное отношение переходов;

 F  Q – множество допускающих состояний.

Опишем алгоритм Герта, Пеледа, Варди и Волпера [16, 17] для

построения автомата Бюхи по LTL-формуле. Введем новый

темпоральный оператор R (Release), который определяется

следующим образом:

φ R ψ = (φ U ψ).

Для него верно, например, аналогичное тождество расширения:

φ R ψ  ψ  (φ  X(φ R ψ)).

Для работы алгоритма требуется, чтобы LTL-формула была приведена

в негативную нормальную форму – отрицание должно применяться

только к атомарным предложениям.

Опишем метод приведения LTL-формулы к негативной нормальной

форме.

1. Заменим все подформулы вида F φ на true U φ.

2. Заменим все подформулы вида G φ на false R φ.

3. Используя булевы тождества, оставим в формуле только три

логические операции: , , .

4. Используя тождества LTL

 (φ U ψ)  φ R ψ,

 (φ R ψ)  φ U ψ и

 X φ  X φ,

погружаем отрицания внутрь темпоральных операторов.

Для алгоритма потребуются следующие структуры данных:

 UID – уникальный идентификатор;

 Formula – LTL-формула;

 Node – вершина графа переходов автомата Бюхи.

Для алгоритма неважно, в каком виде будут представлены

уникальные идентификаторы и формулы, поэтому опишем только

структуру Node (листинг 2.1):

Листинг 2.1. Структура Node

struct Node

{

UID id;

list<NodeID> incoming;

list<Formula> old;

list<Formula> new;

list<Formula> next;

};

Здесь incoming – список вершин-предшественников (вершин, из

которых идет дуга в текущую вершину). В полях old, new и next

содержатся списки подформул исходной формулы.

Функция CreateAutomaton (листинг 2.2) строит граф переходов

автомата Бюхи по формуле f.

Листинг 2.2. Функция CreateAutomaton

list<Node> CreateAutomaton (Formula f)

{

Node n;

n.incoming = {init};

n.old = ;

n.new = {f};

n.next = ;

return expand(n, );

}

Добавление новой вершины выполняется функцией Expand

(листинг 2.3):

Листинг 2.3. Функция Expand

list<Node> Expand (Node currentNode, list<Node> nodes)

{

if (currentNode.new == )

{

if ( Node r  nodes: r.old == currentNode.old

&& r.next == currentNode.next)

{

r.incoming = r.incoming  currentNode.incoming;

return nodes;

}

else

{

Node newNode;

newNode.incoming = {currentNode};

newNode.old = newNode.next = ;

newNode.new = currentNode.next;

Expand(newNode, nodes  {currentNode});

}

else // currentNode.new не пуст.

{

Выбрать Formula n из currentNode.new;

currentNode.new = currentNode.new \ {n};

if (n  currentNode.old) Expand(currentNode, nodes);

else

{

if (n == false or !n  currentNode.old) return

nodes;

if (n  AP or !n  AP or n == true)

// Замещение вершины.

{

node newNode;

newNode.incoming = currentNode.incoming;

newNode.old = currentNode.old  {n};

newNode.new = currentNode.new;

newNode.next = currentNode.next;

Expand(newNode, nodes);

}

if (n имеет вид f  g)

// Замещение вершины currentNode вершиной newNode.

{

node newNode1, newNode2;

newNode1.incoming = currentNode.incoming;

newNode1.old = currentNode.old  {n};

newNode1.new = currentNode.new  {f};

newNode1.next = currentNode.next;

newNode2.incoming = currentNode.incoming;

newNode2.old = currentNode.old  {n};

newNode2.new = currentNode.new  {g};

newNode2.next = currentNode.next;

Expand(newNode2, Expand(newNode1, nodes));

}

if (n имеет вид f U g)

// f U g  g  (f  X (f U g)).

// Расщепление на две вершины.

{

node newNode1, newNode2;

newNode1.incoming = currentNode.incoming;

newNode1.old = currentNode.old  {n};

newNode1.new = currentNode.new  {f};

newNode1.next = currentNode.next  {f U g};

newNode2.incoming = currentNode.incoming;

newNode2.old = currentNode.old  {n};

newNode2.new = currentNode.new  {g};

newNode2.next = currentNode.next;

Expand(newNode2, expand(newNode1, nodes));

}

if (n имеет вид f R g)

// f R g  g  (f  X (f R g)).

// Расщепление на две вершины.

{

node newNode1, newNode2;

newNode1.incoming = currentNode.incoming;

newNode1.old = currentNode.old  {n};

newNode1.new = currentNode.new  {f};

newNode1.next = currentNode.next;

newNode2.incoming = currentNode.incoming;

newNode2.old = currentNode.old  {n};

newNode2.new = currentNode.new  {f, g};

newNode2.next = currentNode.next  {f R g};

Expand(newNode2, expand(newNode1, nodes));

}

if (n имеет вид f  g)

// Замещение вершины currentNode вершиной newNode.

{

node newNode;

newNode.incoming = currentNode.incoming;

newNode.old = currentNode.old  {n};

newNode.new = currentNode.new  {f, g};

newNode.next = currentNode.next;

Expand(newNode, nodes);

}

if (n имеет вид X f)

// Замещение вершины currentNode вершиной newNode.

{

node newNode;

newNode.incoming = currentNode.incoming;

newNode.old = currentNode.old  {n};

newNode.new = currentNode.new;

newNode.next = currentNode.next  {f};

Expand(newNode, nodes);

}

Пример. Рассмотрим первые несколько шагов алгоритма для

формулы F((p R q)  r). Приведем формулу к негативной нормальной

форме:

F((p R q)  r)  true U ((p R q)  r) 

 true U ((p R q)  r)  true U ((p U q)  r).

Таким образом, на вход алгоритму подается формула

f = true U ((p U q)  r). Создаем вершину init и вершину n. После

этого создадим для вершины n пустые списки old и next и список new,

содержащий формулу f. Далее создаем пустой список nodes, в котором

будут храниться вершины построенного графа переходов автомата

Бюхи.

Запустим функцию Expand и извлечем формулу f из списка n.new.

Формула f имеет вид a U b. Поэтому расщепим вершину n на две

вершины: n

и n

(табл. 2.1).

Таблица 2.1. Расщепление вершины n на вершины n

и n

incoming

init

old



new

true

true U ((p U q)  r)

Далее применяем функцию Expand сначала к вершине n

, а после

этого к построенному этой же функцией списку и вершине n

При извлечении из списка n

.new формулы true вершина n

замещается

вершиной n

(табл. 2.2).

Таблица 2.2. Замещение вершины n

вершиной n

incoming

init

old

{f , true}

new

true



Список new вершины n

пуст. Так как список nodes пуст и не

содержит вершину r, у которой с текущей вершиной совпадают

списки old и next, добавляем в список nodes вершину n

. Создаем

новую вершину n

(табл. 2.3):

Таблица 2.3. Вершина n

incoming

init

old



new

Дальнейшие итерации выполняются тем же способом.

Проверка моделей с использованием автоматов Бюхи

Пусть даны модель Крипке и LTL-формула, выполнение которой на

модели требуется проверить. Общая идея алгоритма следующая:

 Из отрицания LTL-формулы строится эквивалентный ей автомат

Бюхи.

 Модель Крипке также преобразуется в автомат Бюхи.

 Строится третий автомат Бюхи как пересечение первых двух.

Такой автомат будет допускать пути исходной модели, которые не

удовлетворяют LTL-формуле спецификации.

 Если язык, допускаемый построенным автоматом-пересечением,

пуст, то верификация успешна. Если нет, то путь, допускаемый

автоматом-пересечением, является контрпримером.

Сначала строится автомат Бюхи, соответствующий верифицируемой

LTL-формуле. Напомним, что он собой представляет. Автомат Бюхи –

это конечный автомат над бесконечными словами. Переходы автомата

Бюхи помечены предикатами из исходной формулы LTL. Автомат

работает следующим образом. На каждом шаге он берет очередной

набор значений предикатов из последовательности, отражающей

историю работы программы. Используя эти значения, автомат

вычисляет метки на переходах из текущего состояния. Активными

называются те переходы, метки которых были вычислены как true.

Если активных переходов больше одного, автомат

недетерминированно выбирает один из них. Таким образом,

последовательность значений предикатов определяет возможные

наборы переходов в автомате Бюхи.

Пример автомата Бюхи, полученного из формулы LTL, изображен на

рис. 2.14. Формула «GF p» читается как «всегда когда-нибудь p» или

«p будет выполняться бесконечно часто».

¬ p

True

¬ p

Рис. 2.14. Автомат Бюхи для формулы «GF p»

В автомате Бюхи имеется набор допускающих состояний. На рис. 2.14

такое состояние отмечено двойным кругом. Если для некоторой

последовательности значений предикатов возможна такая

последовательность переходов в автомате Бюхи, что допускающие

состояния посещаются бесконечно часто, то говорят, что автомат

допускает эту последовательность значений предикатов.

Формула LTL и автомат Бюхи, построенный из нее, эквивалентны в

том смысле, что если некоторый путь (история работы программы)

удовлетворяет формуле, то он допускается автоматом Бюхи.

И наоборот, любая последовательность значений предикатов,

допускаемая автоматом Бюхи, удовлетворяет исходной формуле LTL.

Поскольку задача верификатора – найти контрпример, автомат Бюхи

строится для отрицания исходной формулы LTL. Таким образом,

автомат Бюхи допускает любые последовательности значений

предикатов, которые не удовлетворяют требованиям.

Для пояснения рассмотрим автомат, изображенный на рис 2.14. Если

существует момент времени, после которого p ни разу не выполнится,

то автомат в этот момент перейдет в допускающее состояние и

останется там навсегда. Таким образом, будет получен допускающий

путь. Автомат Бюхи на рис. 2.14 недетерминирован: возможны два

перехода из недопускающего состояния при невыполнении p. Кроме

того, часто автомат строится неполным: например, если автомат на

рис. 2.14 находится в допускающем состоянии и выполнено p, то не

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

вычисление не допускается. Действительно, при выполнении p

нарушится предположение о том, что, начиная с выбранного момента

времени, p не выполнится ни разу.

Следующий этап для верификации LTL-формулы – это

преобразование модели Крипке в автомат Бюхи. Пример модели

Крипке и автомата, полученного из нее, изображен на рис. 2.15.

При построении автомата из модели Крипке вместо состояний

предикатами помечаются переходы. Это делается достаточно просто:

добавляется одно начальное состояние, из которого создаются

p, q

Рис. 2.15. Пример модели Крипке (а) и ее преобразования в автомат (б)

переходы в начальные состояния исходной модели Крипке. Затем

каждый переход помечается теми предикатами, которые выполняются

в конечном состоянии перехода в исходной модели Крипке. Таким

образом, предикаты переносятся из состояний на переходы. Автомат

Бюхи, полученный в результате, является разновидностью автомата

Мура [17]: метки на переходах зависят только от конечного состояния

перехода.

Любой путь в построенном автомате является одним из возможных

сценариев работы модели Крипке. Поэтому все состояния автомата

помечаются как допускающие. В результате построенный автомат

допускает любую последовательность предикатов, соответствующую

возможному сценарию работы верифицируемой модели. В то же

время любая допускаемая автоматом последовательность является

одним из сценариев работы модели.

После построения автомата по модели Крипке и автомата Бюхи,

создается автомат-пересечение, который, по определению, допускает

только те последовательности предикатов, которые допускаются и

автоматом Бюхи, и моделью Крипке. Построенное пересечение

автоматов также является автоматом Бюхи. При этом если для него

существует допускающий путь, то такой путь:

 является одним из возможных сценариев работы модели;

 нарушает верифицируемую LTL-формулу спецификации.