ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
6 КОМПЬЮТЕРНЫЕ СИСТЕМЫ И ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИ
УДК 004.4’242
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
С.Э. Вельдер, А.А. Шалыто
В статье рассматриваются способы преобразования программ, разработанных на основе автоматного подхода, в модели Крипке, предназначенные для проверки свойств, относящихся к поведению системы. Эти свойства задаются формулами темпоральной логики. Предложен эффективный метод такого преобразования и формулировки указанных свойств, который позволяет строить небольшие модели Крипке и достаточно быстро проводить их проверку. Ключевые слова: верификация моделей, темпоральные логики, Model checking, автоматное программирование.
Введение
В данной работе предлагается метод верификации моделей (Model checking) применительно к автоматным программам. В этом контексте исследуются особенности структуры (модели) Крипке. Причина, по которой этим вопросам уделяется внимание, заключается в преимуществах автоматных программ перед остальными в смысле верификации, так как алгоритмы верификации автоматных программ могут оперировать с моделью Крипке, заданной в явном виде, в то время как для традиционных программ процесс построения модели требует дополнительного исследования. Можно выделить следующие ключевые этапы верификации автоматных программ: преобразование автоматной модели в модель Крипке и построение требований к модели (свойства модели); собственно процесс верификации (отработки алгоритмов на полученных моделях); построение подтверждающих трасс (контрпримеров) в модели Крипке, а также представление контрпримеров, записанных в терминах модели Крипке, в виде путей в исходной автоматной модели. Алгоритмы верификации и построения контрпримеров в модели Крипке изложены в работах [1–5]. Генерация модели Крипке основана на построении редуцированного графа переходов, структура которого рассматривается в данной работе.
Общие положения
В этом разделе описывается метод генерации множества атомарных предложений автоматной программы и преобразования автомата с булевыми входными переменными в модель Крипке. Метод состоит в редукции полного графа переходов с внесением тесных отрицаний внутрь атомарной формулы. Приводится пример записи требований к программе. Требования выражаются в темпоральной логике CTL.
Моделью Крипке (также CTL-моделью) для данного множества атомарных пред-
ложений AP будем считать тройку M = ( S, R, Label ) , где:
− S – непустое множество состояний; → ⊆ S × S – тотальное отношение на S, называемое отношением переходов. Для него
должна выполняться формула ∀s ∈ S ∃s′ ∈ S | ( s, s′ ) ∈→ (свойство тотальности).
Оно сопоставляет каждому элементу (состоянию) s ∈ S непустое множество его состояний-последователей.
66 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
С.Э. Вельдер, А.А. Шалыто
− Label ⊆ S × AP – помечающее отношение, сопоставляющее каждому состоянию s ∈ S множество атомарных предложений, истинных в s. Иногда можно потребовать, чтобы в модели Крипке было задано непустое множе-
ство начальных состояний S0 ⊆ S или даже одно начальное состояние s ∈ S.
Построение модели Крипке по автоматной модели
Рассмотрим программу, модель которой задается системой автоматов, взаимодействующих по вложенности. Необходимо преобразовать эту модель в единую модель Крипке, целиком описывающую поведение данной системы.
Прежде всего для множества автоматов выполняется топологическая сортировка по отношению вложенности. Данное отношение не должно содержать циклов, иначе полученная модель имела бы бесконечный размер. Модель Крипке строится индуктивно для каждого автомата системы, причем автоматы обрабатываются в порядке, который был сформирован топологической сортировкой. Такой порядок означает, что перед обработкой внешних автоматов вложенные в них уже будут обработаны (для них будет подготовлена модель Крипке).
Итак, опишем алгоритм построения модели Крипке для одиночного автомата в предположении, что модели Крипке для всех его вложенных автоматов уже построены. Будем пользоваться терминологией, введенной в разд. 2.2.1.1 отчета по III этапу темы [6].
В методе редукции графа переходов множество AP задается следующим образом: {Y1, Y2, …} ∪ {e1, e2, …} ∪ {x1, x2, …} ∪ {!x1, !x2, …} ∪ {z1, z2, …} ∪ {InState, InEvent, InAction} ∪ Names.
Здесь {Y1, Y2, …} – множество наименований всех состояний автоматов, {e1, e2, …} – событий, {x1, x2, …} – входных воздействий, а {z1, z2, …} – выходных воздействий. Names – множество наименований самих автоматов, а InState, InEvent и InAction – управляющие автомарные предложения, предназначенные для того, чтобы было удобно различать позиции, построенные из состояний, событий и выходных воздействий.
Модель Крипке будем строить по частям: вначале построим те ее части, которые соответствуют состояниям автомата (при этом потребуется обработать выходные воздействия и автоматы, вложенные в эти состояния), а потом добавим туда информацию о переходах. На первом шаге положим множество S равным множеству состояний исходного автомата, и для каждого состояния s добавим в отношение Label две пометки: (s, s) и (s, InState).
После этого для каждого состояния s необходимо выполнить следующую операцию. Пусть s содержит выходные воздействия ,zs[1] …, ,zs[u] которые выполняются при входе в s. Добавим в модель u состояний {r1, …, ru} и u переходов r1 → r2, …, ru-1 → ru, ru → s, в отношение Label добавим пометки (rk, zs[k]), (rk, InAction) для всех k от 1 до u. При добавлении ребер в модель на следующих этапах каждую дугу, направленную в s, будем перенаправлять в r1.
Пример такого преобразования приведен на рис. 1.
Y
z1, z2, …, zn
аб
Рис. 1. Состояние с выходными воздействиями до преобразования (а) и после него (б)
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
67
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
Назовем эту операцию разделением выходных переменных и состояний. Теперь следует отделить состояния от вложенных в них автоматов.
Пусть в состояние Y внешнего автомата вложены автоматы AY,1, AY,2, …, AY,v (для них модели Крипке уже построены по индуктивному предположению). В модели Крипке для внешнего автомата (которая еще строится) уже присутствует позиция, соответствующая состоянию Y. Для каждого из автоматов AY,1, AY,2, …, AY,v добавим его модель Крипке к строящейся модели Крипке внешнего автомата. При добавлении требуется скопировать во внешнюю модель Крипке все состояния, переходы и пометки внутренней модели Крипке. Для каждого состояния внутренней модели Крипке создадим уникальное, соответствующее только ему, состояние внешней модели Крипке. Во внешнее отношение переходов → добавим переходы между теми состояниями, которые соответствовали всем переходам между состояниями внутренней модели. Аналогично поступим и с помечающим отношением Label.
После того, как внутренние модели Крипке будут скопированы во внешнюю, добавим в нее также v переходов: для каждого i от 1 до v – 1 добавим в отношение → переход из терминальной позиции модели Крипке для автомата AY,i в стартовую позицию модели Крипке для автомата ,AY,i+1 а также один переход из терминальной позиции модели Крипке для автомата AY,v в позицию, соответствующую состоянию Y. Если до этого в позицию Y вели какие-либо дуги, то все они перенаправляются в стартовую позицию модели Крипке для автомата AY,1.
Пример такого преобразования приведен на рис. 2.
Рис. 2. Обработка автоматов, вложенных в состояние
Обратим внимание, что в различные состояния автомата A могут быть вложены различные «копии» одного и того же автомата B. В этом случае для каждой копии автомата создается своя модель Крипке (все эти модели изоморфны друг другу), и перенаправление дуг выполняется для нее. Размер полученной модели Крипке (число ее состояний) будет ограничен сверху произведением размеров моделей Крипке для каждого автомата в отдельности (без учета вложенных).
На данном этапе закончивается обработка состояний автомата. Поэтому перейдем к описанию того, как обрабатываются переходы.
Рассмотрим множество следующих символов: {x1, !x1; x2, !x2; x3, !x3; …}. Можно сказать, что это множество всех литералов, составленных из входных переменных. Следует различать смысл знаков ¬ и !. Первый из них означает выполнение операции логического отрицания, а второй интерпретируется просто как символ (часть строки !xi).
Тогда для каждого ребра r исходного автомата, ведущего из состояния p в состояние q с пометкой ei & hj[1]& hj[2]& hj[3]& … hj[m] / ,zi[1] …, ,zi[n] где либо = ,hj[j*] xj[j*] либо hj[j*] = !xj[j*] (это значит, что hj[j*] есть либо входная переменная, либо ее отрицание), добавим в модель n + 1 состояние {re, r1, …, rn}, n + 2 перехода: p → re, re → r1, r1 → r2, …, rn-1 → rn, rn → q, а в отношение Label добавим пометки (re, ei),
68 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
С.Э. Вельдер, А.А. Шалыто
(re, InEvent), (rk, zi[k]), (rk, InAction) для всех k от 1 до n, а также пометки (re, hj[1]), (re, hj[2]), …, (re, hj[m]).
Пример такого преобразования отражен на рис. 3.
а
б
Рис. 3. Переход между состояниями до преобразования по методу редукции (а) и после него (б)
Из этого рисунка видно, что для тех состояний, которые были построены из событий, в множество атомарных предложений были добавлены входные переменные в том виде, в котором они записаны на переходах автомата (вместе с отрицаниями, если имеются).
Далее для каждой внешней позиции полученной модели (внешней будем называть любую позицию, за исключением тех, которые были скопированы при обработке вложенных автоматов) добавим в отношение Label пометку с атомарным предложением (элементом множества Names), соответствующим имени обрабатываемого автомата (того, для которого строится модель и которому это состояние принадлежит). Эти действия предназначены для того, чтобы в формулах темпоральной логики можно было различать какой именно из автоматов системы выполняется на данном участке пути.
Если на переходах каких-либо автоматов указаны условия на состояния других автоматов, то эти переходы следует добавлять в модель Крипке только в случае, если данные условия соблюдаются. Так как автоматы вложены друг в друга, то следует проверять условия на переходах внутренних автоматов, описывающие поведение внешних автоматов. Пример построения модели Крипке по системе взаимодействующих автоматов приведен на рис. 4.
Рис. 4. Система автоматов, взаимодействующих по вложенности, с условиями на состояниях внешних автоматов и модель Крипке для этой системы
Рассмотрим пример работы этого алгоритма для системы, эмулирующей работу банкомата [6, 7]. Система состоит из двух автоматов AClient и AServer, причем AServ-
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
69
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
er вложен в AClient. Схема связей для соответствующей автоматной модели изображена на рис. 5, а графы переходов автоматов AServer и AClient – соответственно на рис. 6 и 7.
Для этой системы модель Крипке имеет большой размер. Поэтому она отображена на рис. 8 в упрощенном виде: позиции модели Крипке не выделяются каждая в свой блок, но видны особенности обработки вложенных автоматов.
{Нажали «выключить»}
pin код неверный}
Рис. 5. Схема связей автоматной модели
70 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
С.Э. Вельдер, А.А. Шалыто
Рис. 6. Граф переходов автомата AClient
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
71
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
Рис. 7. Граф переходов автомата AServer
Рис. 8. Редукция графа переходов для модели банкомата
72 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
С.Э. Вельдер, А.А. Шалыто
Проверка CTL-формулы Разберем построение и интерпретацию CTL-формул для редуцированных моделей.
Рис. 9. Пример пути в модели Крипке для банкомата
CTL-семантика в данном методе будет немного отличаться от общепринятой: перед тем, как выполнять верификацию CTL-формулы, ее следует привести к определенному («каноническому») виду. Вначале в ней необходимо удалить все парные отрицания (путем замены подформул вида ¬¬f на f). После этого все входные воздействия, которые присутствуют в формуле без отрицания, требуется предварить двумя отрицаниями: одно из них – синтаксическое, другое – логическое (это значит, что необходимо заменить литералы вида xi на формулы ¬!xi). Только после этих модификаций результирующую формулу можно верифицировать методами, предназначенными для языка CTL. Причина такого обращения с литералами заключается в следующем: требуется обеспечить, чтобы любая ссылка на несущественную переменную, которая упомянута в CTL-формуле, давала истинный результат (несущественными переменными на данном переходе называются те входные переменные исходного автомата, значение которых не проверяется на этом переходе).
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
73
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
Рассмотрим пример для модели банкомата. Проверим CTL-формулу:
e14 → ¬E[ ¬o3.z0 U y10 ] . Она означает: если произошло событие e14, то невозможно
попасть в состояние 10, минуя позицию o3.z0. Эта формула верна во всех позициях модели. Все пути из позиции e14 в состояние 10 дважды «проходят» через автомат AServer: в первый раз – попав в состояние 3, а второй – попав в состояние 9 автомата AClient. Пример такого пути (не проходящего дважды через одно состояние одного и того же экземпляра автомата) выделен на рис. 9. Позиция e14, являющаяся стартовой для данного пути, выделена на рисунке жирным шрифтом.
Рис. 10. Участок пути в автомате AClient
Таким образом, в методе редукции графа переходов была видоизменена семантика CTL. Рассмотренная схема преобразовывала исходную формулу, построенную для но74 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
С.Э. Вельдер, А.А. Шалыто
вой семантики CTL, в новую формулу, для которой применима общепринятая семантика языка CTL. Использование такой схемы подходит для многих формул.
Путь в модели Крипке для банкомата, отображенный на рис. 9, можно показать и в терминах исходной системы автоматов (рис. 10, 11).
а
б
Рис. 11. Участок пути в автомате AServer при первом прохождении (а) и при втором прохождении (б)
Преобразование сценария для модели Крипке в сценарий для автомата
После моделирования и верификации требуется обработать результаты проверки модели. Программы, написанные с помощью традиционных методов, имеют достаточно сложные модели, и проводить анализ путей прямо на модели Крипке неэффективно.
При интерактивном моделировании совместно с исполнением и визуализацией автомата [8, 9] желательно автоматизировать процесс представления путей в модели Крипке путями в автомате.
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
75
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
После того, как отработала программа-верификатор, необходимо определить выполнимость формул, которые формируют спецификацию на заданных участках автомата. Среди этих участков могут быть состояния, события, выходные воздействия.
Сценарий для любой подформулы спецификации представляет собой путь в модели Крипке, иллюстрирующий справедливость или ошибочность данной подформулы. Задача состоит в том, чтобы сценарий, представленный программой для модели Крипке, был представлен в исходном автомате.
Для описанного в настоящей работе метода операция переноса путей из модели Крипке в автомат выполняется однозначно. Действительно, состояния модели, содержащие атомарное предложение Y =… или вспомогательное атомарное предложение InState, однозначно преобразуются в соответствующие им состояния автомата. Путь между любыми двумя соседними состояниями всегда представляет собой «змейку» из события и выходных воздействий. Любая из этих промежуточных позиций однозначно определяет то главное состояние автомата, из которого эта «змейка» исходит. Из атомарных предложений, которыми помечены состояния «змейки», однозначно восстанавливаются события. Значения существенных входных переменных (тех, которые записаны на переходе) и список несущественных переменных определяется оттуда же (методом редукции). Последовательным проходом по полученному пути восстанавливается информация о выполнимости литералов, соответствующих выходным воздействиям, об очередности этих литералов и о том, как попасть в данное состояние.
Заключение
В работе предложен метод редукции графа переходов для представления системы автоматов структурами Крипке. Этот метод реализован программно. Программа позволяет строить трассы, которые подтверждают заданные формулы, начинающиеся с квантора существования пути (или опровергают отрицания этих формул). Рассмотренные примеры показывают, что предложенный метод позволяет убеждаться в корректности модели, находить ошибки в случае некорректных формул и ошибки в неверной модели. Ряд тестов проводился для намеренно измененной модели, чтобы продемонстрировать эффективность метода.
Литература
1. Emerson E.A., Clarke E.M. Using branching time temporal logic to synthesize synchronization skeletons // Science of Computer Programming. – 1982. – № 2. – Р. 241–266.
2. Clarke E.M., Emerson E.A. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic // Logics of Programs, Workshop. – Yorktown Heights, New York, May 1981. – LNC, 131. –Springer, 1982. – Р. 52–71.
3. Лифшиц Ю. Верификация программ и темпоральные логики. Лекция №3 курса «Современные задачи теоретической информатики». – СПбГУ ИТМО, 2005 [Электронный ресурс]. – Режим доступа: http://logic.pdmi.ras.ru/~yura/modern/03modernnote.pdf, свободный.
4. Лифшиц Ю. Символьная верификация программ. Лекция № 4 курса «Современные задачи теоретической информатики». – СПбГУ ИТМО, 2005 [Электронный ресурс].– Режим доступа: http://logic.pdmi.ras.ru/~yura/modern/04modernnote.pdf, свободный
5. Вельдер С.Э., Шалыто А.А. О верификации автоматных программ на основе метода Model Checking // Информационно-управляющие системы. – 2007. – № 3. – С. 27– 38.
76 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
И.А. Бессмертный
6. Разработка технологии верификации управляющих программ со сложным поведением, построенным на основе автоматного подхода. Отчеты по НИР, выполняемая по государственному контракту № 02.514.11.4048 от 18.05.2007 [Электронный ресурс]. – Режим доступа: http://is.ifmo.ru/verification/, свободный.
7. Козлов В.А., Комалева О.А. Моделирование работы банкомата. – СПбГУ ИТМО, 2006 [Электронный ресурс]. – Режим доступа: http://is.ifmo.ru/unimodprojects/bankomat/, свободный.
8. Сайт проекта UniMod [Электронный ресурс]. – Режим доступа: http://unimod.sf.net, свободный.
9. Сайт eVelopers Corporation [Электронный ресурс]. – Режим доступа: http://www.evelopers.com, свободный.
Вельдер Сергей Эдуардович Шалыто Анатолий Абрамович
– Санкт-Петербургский государственный университет информационных технологий, механики и оптики, магистр прикладной математики и информатики, аспирант, velder@rain.ifmo.ru
– Санкт-Петербургский государственный университет информационных технологий, механики и оптики, доктор технических наук, профессор, заведующий кафедрой, shalyto@mail.ifmo.ru
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
77
6 КОМПЬЮТЕРНЫЕ СИСТЕМЫ И ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИ
УДК 004.4’242
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
С.Э. Вельдер, А.А. Шалыто
В статье рассматриваются способы преобразования программ, разработанных на основе автоматного подхода, в модели Крипке, предназначенные для проверки свойств, относящихся к поведению системы. Эти свойства задаются формулами темпоральной логики. Предложен эффективный метод такого преобразования и формулировки указанных свойств, который позволяет строить небольшие модели Крипке и достаточно быстро проводить их проверку. Ключевые слова: верификация моделей, темпоральные логики, Model checking, автоматное программирование.
Введение
В данной работе предлагается метод верификации моделей (Model checking) применительно к автоматным программам. В этом контексте исследуются особенности структуры (модели) Крипке. Причина, по которой этим вопросам уделяется внимание, заключается в преимуществах автоматных программ перед остальными в смысле верификации, так как алгоритмы верификации автоматных программ могут оперировать с моделью Крипке, заданной в явном виде, в то время как для традиционных программ процесс построения модели требует дополнительного исследования. Можно выделить следующие ключевые этапы верификации автоматных программ: преобразование автоматной модели в модель Крипке и построение требований к модели (свойства модели); собственно процесс верификации (отработки алгоритмов на полученных моделях); построение подтверждающих трасс (контрпримеров) в модели Крипке, а также представление контрпримеров, записанных в терминах модели Крипке, в виде путей в исходной автоматной модели. Алгоритмы верификации и построения контрпримеров в модели Крипке изложены в работах [1–5]. Генерация модели Крипке основана на построении редуцированного графа переходов, структура которого рассматривается в данной работе.
Общие положения
В этом разделе описывается метод генерации множества атомарных предложений автоматной программы и преобразования автомата с булевыми входными переменными в модель Крипке. Метод состоит в редукции полного графа переходов с внесением тесных отрицаний внутрь атомарной формулы. Приводится пример записи требований к программе. Требования выражаются в темпоральной логике CTL.
Моделью Крипке (также CTL-моделью) для данного множества атомарных пред-
ложений AP будем считать тройку M = ( S, R, Label ) , где:
− S – непустое множество состояний; → ⊆ S × S – тотальное отношение на S, называемое отношением переходов. Для него
должна выполняться формула ∀s ∈ S ∃s′ ∈ S | ( s, s′ ) ∈→ (свойство тотальности).
Оно сопоставляет каждому элементу (состоянию) s ∈ S непустое множество его состояний-последователей.
66 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
С.Э. Вельдер, А.А. Шалыто
− Label ⊆ S × AP – помечающее отношение, сопоставляющее каждому состоянию s ∈ S множество атомарных предложений, истинных в s. Иногда можно потребовать, чтобы в модели Крипке было задано непустое множе-
ство начальных состояний S0 ⊆ S или даже одно начальное состояние s ∈ S.
Построение модели Крипке по автоматной модели
Рассмотрим программу, модель которой задается системой автоматов, взаимодействующих по вложенности. Необходимо преобразовать эту модель в единую модель Крипке, целиком описывающую поведение данной системы.
Прежде всего для множества автоматов выполняется топологическая сортировка по отношению вложенности. Данное отношение не должно содержать циклов, иначе полученная модель имела бы бесконечный размер. Модель Крипке строится индуктивно для каждого автомата системы, причем автоматы обрабатываются в порядке, который был сформирован топологической сортировкой. Такой порядок означает, что перед обработкой внешних автоматов вложенные в них уже будут обработаны (для них будет подготовлена модель Крипке).
Итак, опишем алгоритм построения модели Крипке для одиночного автомата в предположении, что модели Крипке для всех его вложенных автоматов уже построены. Будем пользоваться терминологией, введенной в разд. 2.2.1.1 отчета по III этапу темы [6].
В методе редукции графа переходов множество AP задается следующим образом: {Y1, Y2, …} ∪ {e1, e2, …} ∪ {x1, x2, …} ∪ {!x1, !x2, …} ∪ {z1, z2, …} ∪ {InState, InEvent, InAction} ∪ Names.
Здесь {Y1, Y2, …} – множество наименований всех состояний автоматов, {e1, e2, …} – событий, {x1, x2, …} – входных воздействий, а {z1, z2, …} – выходных воздействий. Names – множество наименований самих автоматов, а InState, InEvent и InAction – управляющие автомарные предложения, предназначенные для того, чтобы было удобно различать позиции, построенные из состояний, событий и выходных воздействий.
Модель Крипке будем строить по частям: вначале построим те ее части, которые соответствуют состояниям автомата (при этом потребуется обработать выходные воздействия и автоматы, вложенные в эти состояния), а потом добавим туда информацию о переходах. На первом шаге положим множество S равным множеству состояний исходного автомата, и для каждого состояния s добавим в отношение Label две пометки: (s, s) и (s, InState).
После этого для каждого состояния s необходимо выполнить следующую операцию. Пусть s содержит выходные воздействия ,zs[1] …, ,zs[u] которые выполняются при входе в s. Добавим в модель u состояний {r1, …, ru} и u переходов r1 → r2, …, ru-1 → ru, ru → s, в отношение Label добавим пометки (rk, zs[k]), (rk, InAction) для всех k от 1 до u. При добавлении ребер в модель на следующих этапах каждую дугу, направленную в s, будем перенаправлять в r1.
Пример такого преобразования приведен на рис. 1.
Y
z1, z2, …, zn
аб
Рис. 1. Состояние с выходными воздействиями до преобразования (а) и после него (б)
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
67
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
Назовем эту операцию разделением выходных переменных и состояний. Теперь следует отделить состояния от вложенных в них автоматов.
Пусть в состояние Y внешнего автомата вложены автоматы AY,1, AY,2, …, AY,v (для них модели Крипке уже построены по индуктивному предположению). В модели Крипке для внешнего автомата (которая еще строится) уже присутствует позиция, соответствующая состоянию Y. Для каждого из автоматов AY,1, AY,2, …, AY,v добавим его модель Крипке к строящейся модели Крипке внешнего автомата. При добавлении требуется скопировать во внешнюю модель Крипке все состояния, переходы и пометки внутренней модели Крипке. Для каждого состояния внутренней модели Крипке создадим уникальное, соответствующее только ему, состояние внешней модели Крипке. Во внешнее отношение переходов → добавим переходы между теми состояниями, которые соответствовали всем переходам между состояниями внутренней модели. Аналогично поступим и с помечающим отношением Label.
После того, как внутренние модели Крипке будут скопированы во внешнюю, добавим в нее также v переходов: для каждого i от 1 до v – 1 добавим в отношение → переход из терминальной позиции модели Крипке для автомата AY,i в стартовую позицию модели Крипке для автомата ,AY,i+1 а также один переход из терминальной позиции модели Крипке для автомата AY,v в позицию, соответствующую состоянию Y. Если до этого в позицию Y вели какие-либо дуги, то все они перенаправляются в стартовую позицию модели Крипке для автомата AY,1.
Пример такого преобразования приведен на рис. 2.
Рис. 2. Обработка автоматов, вложенных в состояние
Обратим внимание, что в различные состояния автомата A могут быть вложены различные «копии» одного и того же автомата B. В этом случае для каждой копии автомата создается своя модель Крипке (все эти модели изоморфны друг другу), и перенаправление дуг выполняется для нее. Размер полученной модели Крипке (число ее состояний) будет ограничен сверху произведением размеров моделей Крипке для каждого автомата в отдельности (без учета вложенных).
На данном этапе закончивается обработка состояний автомата. Поэтому перейдем к описанию того, как обрабатываются переходы.
Рассмотрим множество следующих символов: {x1, !x1; x2, !x2; x3, !x3; …}. Можно сказать, что это множество всех литералов, составленных из входных переменных. Следует различать смысл знаков ¬ и !. Первый из них означает выполнение операции логического отрицания, а второй интерпретируется просто как символ (часть строки !xi).
Тогда для каждого ребра r исходного автомата, ведущего из состояния p в состояние q с пометкой ei & hj[1]& hj[2]& hj[3]& … hj[m] / ,zi[1] …, ,zi[n] где либо = ,hj[j*] xj[j*] либо hj[j*] = !xj[j*] (это значит, что hj[j*] есть либо входная переменная, либо ее отрицание), добавим в модель n + 1 состояние {re, r1, …, rn}, n + 2 перехода: p → re, re → r1, r1 → r2, …, rn-1 → rn, rn → q, а в отношение Label добавим пометки (re, ei),
68 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
С.Э. Вельдер, А.А. Шалыто
(re, InEvent), (rk, zi[k]), (rk, InAction) для всех k от 1 до n, а также пометки (re, hj[1]), (re, hj[2]), …, (re, hj[m]).
Пример такого преобразования отражен на рис. 3.
а
б
Рис. 3. Переход между состояниями до преобразования по методу редукции (а) и после него (б)
Из этого рисунка видно, что для тех состояний, которые были построены из событий, в множество атомарных предложений были добавлены входные переменные в том виде, в котором они записаны на переходах автомата (вместе с отрицаниями, если имеются).
Далее для каждой внешней позиции полученной модели (внешней будем называть любую позицию, за исключением тех, которые были скопированы при обработке вложенных автоматов) добавим в отношение Label пометку с атомарным предложением (элементом множества Names), соответствующим имени обрабатываемого автомата (того, для которого строится модель и которому это состояние принадлежит). Эти действия предназначены для того, чтобы в формулах темпоральной логики можно было различать какой именно из автоматов системы выполняется на данном участке пути.
Если на переходах каких-либо автоматов указаны условия на состояния других автоматов, то эти переходы следует добавлять в модель Крипке только в случае, если данные условия соблюдаются. Так как автоматы вложены друг в друга, то следует проверять условия на переходах внутренних автоматов, описывающие поведение внешних автоматов. Пример построения модели Крипке по системе взаимодействующих автоматов приведен на рис. 4.
Рис. 4. Система автоматов, взаимодействующих по вложенности, с условиями на состояниях внешних автоматов и модель Крипке для этой системы
Рассмотрим пример работы этого алгоритма для системы, эмулирующей работу банкомата [6, 7]. Система состоит из двух автоматов AClient и AServer, причем AServ-
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
69
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
er вложен в AClient. Схема связей для соответствующей автоматной модели изображена на рис. 5, а графы переходов автоматов AServer и AClient – соответственно на рис. 6 и 7.
Для этой системы модель Крипке имеет большой размер. Поэтому она отображена на рис. 8 в упрощенном виде: позиции модели Крипке не выделяются каждая в свой блок, но видны особенности обработки вложенных автоматов.
{Нажали «выключить»}
pin код неверный}
Рис. 5. Схема связей автоматной модели
70 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
С.Э. Вельдер, А.А. Шалыто
Рис. 6. Граф переходов автомата AClient
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
71
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
Рис. 7. Граф переходов автомата AServer
Рис. 8. Редукция графа переходов для модели банкомата
72 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
С.Э. Вельдер, А.А. Шалыто
Проверка CTL-формулы Разберем построение и интерпретацию CTL-формул для редуцированных моделей.
Рис. 9. Пример пути в модели Крипке для банкомата
CTL-семантика в данном методе будет немного отличаться от общепринятой: перед тем, как выполнять верификацию CTL-формулы, ее следует привести к определенному («каноническому») виду. Вначале в ней необходимо удалить все парные отрицания (путем замены подформул вида ¬¬f на f). После этого все входные воздействия, которые присутствуют в формуле без отрицания, требуется предварить двумя отрицаниями: одно из них – синтаксическое, другое – логическое (это значит, что необходимо заменить литералы вида xi на формулы ¬!xi). Только после этих модификаций результирующую формулу можно верифицировать методами, предназначенными для языка CTL. Причина такого обращения с литералами заключается в следующем: требуется обеспечить, чтобы любая ссылка на несущественную переменную, которая упомянута в CTL-формуле, давала истинный результат (несущественными переменными на данном переходе называются те входные переменные исходного автомата, значение которых не проверяется на этом переходе).
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
73
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
Рассмотрим пример для модели банкомата. Проверим CTL-формулу:
e14 → ¬E[ ¬o3.z0 U y10 ] . Она означает: если произошло событие e14, то невозможно
попасть в состояние 10, минуя позицию o3.z0. Эта формула верна во всех позициях модели. Все пути из позиции e14 в состояние 10 дважды «проходят» через автомат AServer: в первый раз – попав в состояние 3, а второй – попав в состояние 9 автомата AClient. Пример такого пути (не проходящего дважды через одно состояние одного и того же экземпляра автомата) выделен на рис. 9. Позиция e14, являющаяся стартовой для данного пути, выделена на рисунке жирным шрифтом.
Рис. 10. Участок пути в автомате AClient
Таким образом, в методе редукции графа переходов была видоизменена семантика CTL. Рассмотренная схема преобразовывала исходную формулу, построенную для но74 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
С.Э. Вельдер, А.А. Шалыто
вой семантики CTL, в новую формулу, для которой применима общепринятая семантика языка CTL. Использование такой схемы подходит для многих формул.
Путь в модели Крипке для банкомата, отображенный на рис. 9, можно показать и в терминах исходной системы автоматов (рис. 10, 11).
а
б
Рис. 11. Участок пути в автомате AServer при первом прохождении (а) и при втором прохождении (б)
Преобразование сценария для модели Крипке в сценарий для автомата
После моделирования и верификации требуется обработать результаты проверки модели. Программы, написанные с помощью традиционных методов, имеют достаточно сложные модели, и проводить анализ путей прямо на модели Крипке неэффективно.
При интерактивном моделировании совместно с исполнением и визуализацией автомата [8, 9] желательно автоматизировать процесс представления путей в модели Крипке путями в автомате.
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
75
ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
После того, как отработала программа-верификатор, необходимо определить выполнимость формул, которые формируют спецификацию на заданных участках автомата. Среди этих участков могут быть состояния, события, выходные воздействия.
Сценарий для любой подформулы спецификации представляет собой путь в модели Крипке, иллюстрирующий справедливость или ошибочность данной подформулы. Задача состоит в том, чтобы сценарий, представленный программой для модели Крипке, был представлен в исходном автомате.
Для описанного в настоящей работе метода операция переноса путей из модели Крипке в автомат выполняется однозначно. Действительно, состояния модели, содержащие атомарное предложение Y =… или вспомогательное атомарное предложение InState, однозначно преобразуются в соответствующие им состояния автомата. Путь между любыми двумя соседними состояниями всегда представляет собой «змейку» из события и выходных воздействий. Любая из этих промежуточных позиций однозначно определяет то главное состояние автомата, из которого эта «змейка» исходит. Из атомарных предложений, которыми помечены состояния «змейки», однозначно восстанавливаются события. Значения существенных входных переменных (тех, которые записаны на переходе) и список несущественных переменных определяется оттуда же (методом редукции). Последовательным проходом по полученному пути восстанавливается информация о выполнимости литералов, соответствующих выходным воздействиям, об очередности этих литералов и о том, как попасть в данное состояние.
Заключение
В работе предложен метод редукции графа переходов для представления системы автоматов структурами Крипке. Этот метод реализован программно. Программа позволяет строить трассы, которые подтверждают заданные формулы, начинающиеся с квантора существования пути (или опровергают отрицания этих формул). Рассмотренные примеры показывают, что предложенный метод позволяет убеждаться в корректности модели, находить ошибки в случае некорректных формул и ошибки в неверной модели. Ряд тестов проводился для намеренно измененной модели, чтобы продемонстрировать эффективность метода.
Литература
1. Emerson E.A., Clarke E.M. Using branching time temporal logic to synthesize synchronization skeletons // Science of Computer Programming. – 1982. – № 2. – Р. 241–266.
2. Clarke E.M., Emerson E.A. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic // Logics of Programs, Workshop. – Yorktown Heights, New York, May 1981. – LNC, 131. –Springer, 1982. – Р. 52–71.
3. Лифшиц Ю. Верификация программ и темпоральные логики. Лекция №3 курса «Современные задачи теоретической информатики». – СПбГУ ИТМО, 2005 [Электронный ресурс]. – Режим доступа: http://logic.pdmi.ras.ru/~yura/modern/03modernnote.pdf, свободный.
4. Лифшиц Ю. Символьная верификация программ. Лекция № 4 курса «Современные задачи теоретической информатики». – СПбГУ ИТМО, 2005 [Электронный ресурс].– Режим доступа: http://logic.pdmi.ras.ru/~yura/modern/04modernnote.pdf, свободный
5. Вельдер С.Э., Шалыто А.А. О верификации автоматных программ на основе метода Model Checking // Информационно-управляющие системы. – 2007. – № 3. – С. 27– 38.
76 Научно-технический вестник Санкт-Петербургского государственного университета
информационных технологий, механики и оптики, 2009, № 6(64)
И.А. Бессмертный
6. Разработка технологии верификации управляющих программ со сложным поведением, построенным на основе автоматного подхода. Отчеты по НИР, выполняемая по государственному контракту № 02.514.11.4048 от 18.05.2007 [Электронный ресурс]. – Режим доступа: http://is.ifmo.ru/verification/, свободный.
7. Козлов В.А., Комалева О.А. Моделирование работы банкомата. – СПбГУ ИТМО, 2006 [Электронный ресурс]. – Режим доступа: http://is.ifmo.ru/unimodprojects/bankomat/, свободный.
8. Сайт проекта UniMod [Электронный ресурс]. – Режим доступа: http://unimod.sf.net, свободный.
9. Сайт eVelopers Corporation [Электронный ресурс]. – Режим доступа: http://www.evelopers.com, свободный.
Вельдер Сергей Эдуардович Шалыто Анатолий Абрамович
– Санкт-Петербургский государственный университет информационных технологий, механики и оптики, магистр прикладной математики и информатики, аспирант, velder@rain.ifmo.ru
– Санкт-Петербургский государственный университет информационных технологий, механики и оптики, доктор технических наук, профессор, заведующий кафедрой, shalyto@mail.ifmo.ru
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2009, № 6(64)
77