автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Генерация управляющих автоматов на основе генетического программирования и верификации

На правах рукописи

Егоров Кирилл Викторович

Генерация управляющих автоматов на основе генетического программирования и верификации

Специальность 05.13.11. Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата технических наук

2 8 НОЯ 2013

Санкт-Петербург-2013 г. 005540770

005540770

Работа выполнена на кафедре «Компьютерные технологии» Санкт-Петербургского национального исследовательского университета информационных технологий, механики и оптики (НИУ ИТМО).

Научный руководитель доктор технических наук,

профессор

Шалыто Анатолий Абрамович

Официальные оппоненты

Ведущая организация

Соколов Валерий Анатольевич, доктор физико-математических наук, профессор, заведующий кафедрой «Теоретическая информатика» Ярославского государственного университета им. П.Г. Демидова

Новиков Федор Александрович, доктор технических наук, профессор кафедры «Прикладная математика» Санкт-

Петербургского государственного

политехнического университета

Санкт-Петербургский институт информатики и автоматизации Российской академии наук

Защита диссертации состоится 25 декабря 2013 года в 15 часов 30 минут на заседании диссертационного совета Д 212.227.06 при НИУ ИТМО по адресу: 197101, Санкт-Петербург, Кронверкский пр., д. 49, конференц-зал Центра Интернет-образования.

С диссертацией можно ознакомиться в библиотеке НИУ ИТМО. Автореферат разослан «21» ноября 2013 года.

Ученый секретарь диссертационного совета

И.С. Лобанов

Общая характеристика работы

Актуальность проблемы. Существуют программы, в которых ошибки могут обойтись слишком дорого. Например, в программах управления транспортом, медицинским оборудованием, военном техникой и другими объектами ошибки могут привести к гибели людей или большим финансовым потерям. Для обеспечения корректности и надежности работы таких объектов большое значение имеют методы, позволяющие выявлять ошибки на разных этапах разработки и сопровождения программного обеспечения для того, чтобы устранять их.

Одним из основных методов проверки программного обеспечения является тестирование. Оно применяется на практике в большинстве случаев. Однако тестирование позволяет находить ошибки, но не доказывает их отсутствие.

Указанную проблему решает верификация - метод доказательства того, что программа соответствует спецификации. На практике часто используется метод, который называется верификацией на моделях (Mode! Checking). При этом спецификация задается в виде темпоральных формул, число которых в общем случае не известно. Поэтому соответствие программы спецификации может быть обеспечено, но это не будет доказательством правильности программы. Для программ произвольного вида применение этого метода связано с построением по программе модели. При автоматном программировании указанная проблема снимается, так как проектирование этого класса программ начинается с построения модели -управляющих конечных автоматов, которые далее будем называть автоматами. Это существенно упрощает верификацию таких программ на основе метода Model Checking. Поэтому в дальнейшем будем рассматривать только автоматные программы.

Еще один подход, обеспечивающий высокое качество программ, состоит в повышении уровня автоматизации их построения. Для рассматриваемого класса программ эта задача состоит из двух частей: генерация автоматов по спецификации и генерация кода программы по автоматам. Можно считать, что вторая проблема решена, а первая проблема решена лишь частично. Например, с помощью генетического программирования можно генерировать автоматы. Если удается построить автомат, то при таком подходе он не всегда соответствует спецификации. Для устранения этого недостатка предлагается в ходе выполнения алгоритма генетического программирования проводить верификацию генерируемых автоматов.

Поэтому исследование, объединяющее генетическое программирование и верификацию при построении автоматов, является актуальным.

Цель диссертационной работы - генерации автоматов на основе генетического программирования и верификации.

При этом задачи, решаемые в диссертации, состоят в следующем:

1. Предложить функцию приспособленности, учитывающую верификацию, проводимую в процессе выполнения алгоритма генетического программирования.

2. Разработать операции скрещивания и мутации, учитывающие верификацию.

А '

3. Разработать алгоритм построения автоматов на основе генетического программирования с учетом контрактов, которые являются разновидностью темпоральных формул.

4. Разработать алгоритм построения автоматов на основе генетического программирования по сценариям работы и верификации.

5. Разработать верификатор, приспособленный для поддержки генерации автоматов на основе генетического программирования.

6. Разработать технологию и инструментальное средство для генерации автоматов с помощью генетического программирования и верификации.

Научная новизна. На защиту выносятся следующие новые научные результаты:

1. Предложена функция приспособленности, учитывающая выполнение формулы на части автомата. В известных работах учитывалось только выполнение или невыполнение каждой темпоральной формулы.

2. Операции скрещивания и мутации отличаются от известных тем, что в ходе их выполнения используется верификация.

3. Алгоритм генерации автоматов с учетом контрактов, который позволяет упростить запись некоторых темпоральных формул и ускорить построение автоматов по сравнению с применением темпоральных формул общего вида.

4. Алгоритм генерации автоматов по темпоральным формулам и сценариям работы, который позволяет ускорить построение автоматов по сравнению с применением тестов.

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

Достоверность разработанных алгоритмов, методов и технологий, полученных в диссертации, подтверждается точной постановкой задач, корректным формулированием параметров и результатов работы генетического алгоритма, численными оценками скорости работы различных подходов, путем экспериментальных исследований.

Практическое значение работы состоит в том, что предложенные подходы позволяют генерировать автоматы, которые соответствуют спецификации и не требуют тестирования и верификации как самостоятельных этапов разработки программ.

Внедрение результатов работы. Результаты диссертации были получены при выполнении научно-исследовательских работ на кафедрах «Компьютерные технологии» и «Технологии программирования» НИУ ИТМО по следующим государственным контрактам: «Разработка методов машинного обучения на основе генетических алгоритмов для построения управляющих конечных автоматов» (государственный контракт № П2174 от 09.11.2009 г. по Федеральной целевой программе «Научные и научно-педагогические кадры инновационной России» на 2009-2013 годы), «Применение методов искусственного интеллекта в разработке управляющих программных систем» (государственный контракт № П2236 от 11.11.2009 г. по Федеральной целевой программе «Научные и научно-педагогические кадры инновационной России» на 2009-2013 годы). Результаты, полученные в

диссертации, были внедрены при построении модуля Top Traffic Monitor для определения узлов сети с максимальным трафиком в программном продукте NetFlow Integrator, выпускаемом компанией ООО DBIÍJIOÍ1EPC (Санкт-Петербург). Результаты работы используются в учебном процессе на кафедре «Компьютерные технологии» НИУ ИТМО в курсе «Автоматное программирование».

Апробация результатов работы. Основные результаты диссертации докладывались на следующих конференциях: 32-я конференция молодых ученых и специалистов Института проблем передачи информации им. A.A. Харкевича РАН «Информационные технологии и системы» (2009), VII и VIII межвузовская конференция молодых ученых (СПбГУ ИТМО, 2010, 2011), 14-th Annual Graduate Students Workshop («Genetic and Evolutionary Computation Conference» GECCO-2011, Dublin, ACM, 2011), вторая и третья межвузовская научная конференция по проблемам информатики СПИСОК-2011, СПИСОК-2012 (СПбГУ, 2011, 2012), I Всероссийский конгресс молодых ученых (СПбГУ ИТМО, 2012).

Личный вклад автора. Решение задач диссертации, разработанные алгоритмы и их реализация принадлежат лично автору.

Публикации. По теме диссертации опубликовано 11 печатных работ, три из которых в журналах из перечня ВАК.

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения и четырех приложений. Список литературы содержит 75 наименований. Объем работы - 151 страница, 35 рисунков и 13 таблиц.

Содержание работы

Первая глава описывает основные идеи автоматного программирования, метод верификации Model Checking, который часто применяется на практике для проверки соответствия программы спецификации. Приведены основные принципы верификации автоматных программ с помощью этого метода.

Автоматное программирование - это парадигма программирования, при использовании которой программа или ее фрагмент рассматривается как система автоматизированных объектов управления. Объекты бывают трех типов: система управления, поставщики событий и объекты управления.

Система управления представляет собой управляющий конечный автомат или систему таких автоматов. В диссертации предполагается, что поведение программ задается одним автоматом, а при описании поведения системой автоматов, они могут быть представлены одним автоматом за счет их «произведения». Автомат состоит из множества состояний и переходов между ними. Каждый переход описывается начальным и конечным состояниями, событием, условием, являющимся булевой формулой, и выходными воздействиями, которые могут быть произвольными. События генерируются их поставщиками, а для проверки условия перехода запрашиваются значения входных переменных у объектов управления. Система управления совершает переход по событию и при выполнении условия перехода, вызывая выходные воздействия.

Формально автомат определяется следующим набором <S, Т, Е, X, Z, s0, L>, где

• S(, - начальное состояние;

• S— конечное множество состояний;

• Е-множество событий;

• X— множество булевых входных переменных;

• Z - множество выходных воздействий произвольного вида;

• TcSxExl* y.S - множество переходов;

• L: Т -» 2г - функция выходных воздействий.

В настоящей работе спецификация описывается темпоральными формулами. Они задаются с помощью языка логики линейного времени (Linear Time Logic, LTV), так как он достаточно прост для понимания и записи утверждений об автоматной программе, которая является классической реагирующей (реактивной) системой. Особенности алгоритма верификации с применением L 7Х-формул позволили использовать его при вычислении функции приспособленности, операциях скрещивания и мутации алгоритма генетического программирования. Синтаксис языка LTL включает в себя темпоральные операторы, множество пропозициональных переменных Prop и булевы связки {&, |, -■). Для составления утверждений (формул) о событиях в будущем применяются следующие темпоральные операторы:

• X (neXt), где Хр - предикат р выполняется в следующий момент времени;

• F (in the Future), где Fp - предикат р выполняется в какой-то момент в будущем;

• G (Globally in the future), где Gp - предикат p выполняется в любой момент времени (всегда);

• U (Until), где pUq — предикат q выполняется в некотором состоянии автомата, а во всех предыдущих выполняется предикат р\

• R (Release), где pRq - либо предикат р выполняется в некотором состоянии, а во всех предыдущих выполняется предикат q, либо предикат q выполняется во всех состояниях.

Множество LTL-формул можно задать следующим рекурсивным образом:

® True, False;

• Prop - множество пропозициональных переменных;

• Если (р и ц! - /Л'¿-формулы, то:

о <р&у, <р\у/ и ~чр - формулы; о F<p, Xtp, G<p, (pRy и (plhji — формулы

Управляющий автомат и ¿7Х-формула представимы в виде автомата Бюхи, который формально определяется пятеркой <S, Е, Т, s0, F>:

• s0- начальное состояние;

• S - конечное множество состояний;

• Е- множество меток переходов;

• ТqSxF.xS — множество переходов;

• FcS — множество допускающих состояний.

Путь в графе переходов этого автомата является допускающим, если существует состояние из множества F, принадлежащее данному пути и встречающееся бесконечное число раз.

Известно, что для доказательства выполнимости некоторой ¿/"¿.-формулы необходимо проверить, что автомат пересечения автоматов Бюхи управляющего

автомата и отрицания £7Х-формулы не допускает ни одно слово. Следовательно, для опровержения этой формулы достаточно найти цикл в автомате пересечения, проходящий через допускающее состояние. Обычно для этого применяется двойной обход в глубину (Depth-first search, DFS), так как он позволяет строить автомат пересечения «на лету»: первый из них определят допускающее состояние, а второй -цикл, проходящий через него. Путь из начального состояния в допускающее является контрпримером, опровергающим формулу. На данном пути выполняется отрицание А77.-формулы.

Алгоритм построения автомата Бюхи по /.7£-формуле известен, а алгоритм преобразования автомата управления в автомат Бюхи был предложен на кафедре КТ НИУ ИТМО (http://is.ifmo.ru/verification/ 2007 02 report-verification.pdf). В качестве пропозициональных переменных автомата Бюхи используются предикаты. Предикатом может являться любое утверждение о текущем переходе, которое всегда выполняется независимо от предыдущих переходов. В работе используются следующие предикаты:

• wasEvent(e) - переход совершен по событию е;

• isInState(s) - переход совершен в состояние s;

• wasInState(s) -- переход совершен из состояния s;

• cameToFinalStateQ - при переходе автомат перешел в завершающее состояние;

• wasAction(z) - во время перехода было выполнено выходное воздействие z;

• wasFirstAction(z) - во время перехода первым выполненным выходным воздействием было z.

Поставщики событий и объекты управления не запоминают последовательность переходов и выходных воздействий рассматриваемого автомата. Поэтому в каждый момент времени из текущего состояния автомата может быть совершен любой переход. Преобразование управляющего автомата в автомат Бюхи производится не явно, а в процессе верификации «на лету».

Изложенное реализовано в разработанном автором верификаторе AulomataVerificator, который доступен по адресу:

http://code.google.eom/p/automataverificator/.

Во второй главе излагается алгоритм генерации автоматов по LTL-формулам, тестовым примерам, контрактам и сценариям работы.

Диссертация является продолжением совместных работ автора и Ф.Н. Царева по генерации автоматов по тестовым примерам и £7Х-формулам. Результаты этих работ используются в настоящей диссертации. Они состоят в том, что функция приспособленности и операции скрещивания н мутации не зависят от рассматриваемой задачи. В этих работах формулы учитывались только в функции приспособленности, и вклад каяедой из них был равен нулю или единице. В настоящей работе верификация учитывается при скрещивании и мутации, а при вычислении функции приспособленности вклад каждой формулы принадлежит отрезку [0; 1]. Это приводит к повышению скорости генерации автоматов с учетом верификации.

При генерации автоматов по тестам и £7Х-формулам, исходными данными являются:

• список событий {е/, е2.....е,.};

• список входных переменных {х/, х2, .... jc„.};

» список выходных воздействий {2/, z2, .... z,};

• максимальное ожидаемое число состояний к;

• набор тестов {{Input[1], Answerfl]}. ... {Input[и], AnswerfnJ}};

• набор ¿71-формул.

Результатом работы как известного, так и предлагаемого алгоритмов генетического программирования, является автомат с числом состояний не больше к, который проходит все тесты и удовлетворяет всем ¿7Х-формулам.

В этих алгоритмах каждый тест содержит последовательность событий Input[i], поступающих на вход автомата, и соответствующую ей эталонную последовательность выходных воздействий Answer[i]. Причем заранее не известно отношение между элементами из Input[i] и элементами из Answer[i], Тест с номером i считается пройденным, если, подав на вход последовательность lnput[i], автомат вызовет в точности последовательность из AnswerfiJ.

Особь при генетическом программировании представлена автоматом, который содержит список переходов для каждого из состояний и номер начального состояния. Переходы задаются событиями и числом выходных воздействий, которые необходимо вызвать у объекта управления. Тем самым, в особи не кодируется конкретные выходные воздействия, а только «скелет» автомата (рисунок 1), а конкретные выходные воздействия, вырабатываемые на переходах, определяются с помощью алгоритма расстановки пометок.

,Т/1

Рисунок 1 - Пример «скелета» автомата

Идея алгоритма расстановки выходных воздействий состоит в следующем: каждый из тестовых примеров запускается на «скелете» автомага, для каждого перехода запоминаются выходные воздействия, после прохождения всех тестов выбираются те выходные воздействия для перехода, которые чаше всего встречаются.

Алгоритм генетического программирования содержит три основных компоненты: функция приспособленности и операции мутации и скрещивания. Ниже [ укажем, в чем состоит новизна каждой из них.

Введем новую функцию приспособленности, задаваемую формулой:

А.Г _ ЕР(Ои/рМ[1],А№ЛУег[<]) ^ ™

„,, тах(| ОШриф]\,\Апшеф]\)) , С-Г

г г —(р------г ш----с--.

п т 10 С

Первая ее часть показывает вклад тестов в функцию приспособленности я), вторая — вклад темпоральных свойств (/'/7.71)5 а третья — учитывает число переходов автомата. В формуле используются следующие обозначения:

• а — функция, принимающая значение И, если проходят все тесты, и 0.5ХЛ' - если проходит только часть из них. Здесь М— «важность» тестов;

• у - функция, принимающая значение /V/, если верны все ¿7/,-формулы, и 0.5*М - если выполняется только часть из них, где М - «важность» формул;

® п- число тестов;

• ОШриф] - последовательность выходных воздействий, которую сгенерировал автомат на входе 1прШ[\];

• ЕО(А, В) - редакционное расстояние между строками А и В;

• т - число ¿7Х-формул;

• 7" - число достижимых переходов в автомате;

• /!, - число переходов, для которых 1-ая ¿7Х-формула выполняется;

• Т— число переходов в автомате;

• С - число заведомо большее числа переходов.

Отметим, что первая и третья части формулы были известны, а вторая - новой. Рассмотрим ее более подробно. В диссертации предлагается учитывать вклад каждой

///'¿-формулы как ~, что позволяет численно оценивать выполнение формулы

значением на отрезке [0; I], а не нулем, если формула не выполняется, или единицей при ее выполнении. Значение I, вычисляется в процессе верификации как число переходов, на которых ¿7Т-формула выполнятся. Далее будем называть такие переходы «проверенными». В основе алгоритма верификации лежит двойной обход в глубину, поэтому «проверенными» переходами можно считать все исходящие переходы для состояний, которые «покинул» первый обход в глубину. Эти переходы и состояния не нарушают ¿7Х-формулу. Тогда отношение числа «проверенных» переходов к числу достижимых переходов будет определять, на какой части автомата формула выполняется.

Пусть, например, верифицируется конечный автомат из шести состояний (рисунок 2). Цифрой «1» выделена часть автомата, на которой не удалось обнаружить контрпример («проверенные» переходы), а цифрой «2» - его часть, на которой формула опровергается. Тогда вклад формулы будет 3/7, где три - число

Рисунок 2 - Пример вычисления вклада ЬТЬ-формулы в функцию приспособленности

Мутация применяется к переходам. Она бывает трех видов: заменить конечное состояние перехода, заменит входное событие и изменить число выходных воздействий. В настоящей работе замены с большей вероятностью применяются к

переходам, которые образуют контрпримеры, а ранее они выполнялись для случайных переходов. Благодаря этому повышается вероятность исчезновения контрпримеров, и повышаются шансы новой особи соответствовать большему числу ¿7Х-формул.

В настоящей работе, так же как и в известной, применялись понятия большая и малая мутации. Они позволяют алгоритму генетического программирования покинуть локальный максимум и не накладывать ограничение на число поколений.

Скрещивание происходит путем обмена переходами между двумя особями. Известно, что оно может быть случайным или учитывать прохождение тестов, а в настоящей работе предлагается учитывать «проверенные» переходы. Скрещивание между двумя особями осуществляется следующим образом. Выбираются случайные 10% ¿/'¿-формул, дня которых выполняется пересечение «проверенных» переходов автомата. Из этого множества переходов исключаются те, которые принадлежат контрпримерам. Такие переходы включаются в новую особь без изменений (рисунок 3). Остальные переходы случайным образом распределяются между особями.

«проверенным» переходам

В результате выполнения скрещивания часть конечного автомата, на которой выполняются некоторые формулы, сохраняется. Это позволяет увеличить функцию приспособленности новой особи.

Перейдем к изложению алгоритма генерации автоматов по ЬТЬ-формулам и контрактам. В общем случае контракт состоит из предусловия, постусловия и инварианта, но может содержать только часть из них. При автоматном подходе контракты могут накладываться как на состояния, так и на переходы и группы состояний.

Контракты для автоматов можно определить через ¿ТХ-формулы особого вида. Определим предусловие как формулу 0(Хр: —»р2) - если на следующем шаге выполнено р], то выполнено и р2, постусловие как формулу С(р1 —> Хр2) - если выполнено р/, то на следующем шаге выполнено р2; инвариант как формулу' С(р, —*>Р2) - если выполнено р], то выполнено и р2, где р/ и р2 предикаты. Так как

контракты являются ¿7Х-формулами, то их выполнение проверяется указанным выше верификатором.

В этом верификаторе постусловие и предусловие оказываются эквивалентными с точностью до предикатов на переходах, так как их отрицание представляются «похожими» автоматами Бюхи. Контрактом можно назвать любую ¿/¿'.-формулу, по отрицанию которой строится автомат Бюхи, эквивалентный автомату контракта с точностью до пометок на переходах. На рисунке 4 представлены автоматы для предусловия (а), постусловия (б) и инварианта (в) для перехода по событию е.

з> !р 0)

т О

Э> а 'р (2) б

Рисунок 4 - Автоматы Бюхи, построенные для отрицания /,7Х-формул: врСе — р) (а), в(е -> Хр) (б), 0(е — р) (в)

При верификации произвольных темпоральных свойств заранее не известна их семантика. Это приводит к тому, что, обнаружив контрпример в автомате, невозможно определить, какой именно переход нарушает свойство. Когда автомат строится на основе контрактов, точно известно, какие переходы в контрпримере нарушают его. Для инварианта - последний переход, а для предусловия и постусловия - последний и предпоследний переходы одновременно. Поэтому при скрещивании и мутации предлагается использовать не весь контрпример, а только переходы, нарушающие ¿,71-формулу, что ускоряет построение автомата.

Перейдем к изложению алгоритма построения автоматов на основе генетического программирования по сценариям работы и верификации. В отличие от диссертации Ф.Н. Царева, в которой применялись тестовые примеры, в настоящей работе используются сценарии работы, которые могут быть либо позитивными, либо негативными.

Позитивный сценарий - это последовательность пар (входное воздействие, соответствующий ему список выходных воздействий). Использование таких сценариев не вносит изменений в функцию приспособленности, приведенную выше, однако требуется небольшая модификация представления особи и алгоритма расстановки пометок. Выше было отмечено, что в случае тестовых примеров каждый переход содержит только число выходных воздействий, а не сами воздействия. При использовании сценариев число выходных воздействий перехода не фиксировано. Алгоритм расстановки пометок выбирает то множество выходных воздействий для перехода автомата, которое чаще всего встречается.

Различие между тестами и сценариями показаны на рисунке 5.

ег ег г ёз е4 ев

31, 32, Из, 34, 31, 35, 33

с-1 ег { ез ■ ..! е4 €5 :

Зз зг \ а3, а* | а ^ 35, аз

а б

Рисунок 5 Тестовые примеры (а) и сценарии работы (б)

Негативный сценарий представляет собой последовательность входных воздействий, которая не должна выполняться в автомате. При этом все префиксы негативного сценария выполняются, а только последний переход не совершается.

Вклад каждого негативного сценария в функцию приспособленности ноль, если сценарий не выполняется, -1 - в противном случае. Вклад всех негативных сценариев вычисляется как отношение суммы вкладов каждого сценария к общему числу сценариев. Негативные сценарии используются при скрещивании и мутации аналогично контрактам, когда известно, какой переход автомата нарушаег выполнение контракта. С большей вероятностью мутирует последний переход негативного сценария. Он не может перейти в новую особь без изменений при скрещивании по позитивным сценариям или ¿77,-формулам.

Экспериментальные исследования предложенных подходов проводились для генерации автомата управления часами с будильником и автомата управления дверьми лифта (рисунок 6а). С помощью каждого подхода автоматы строились по 1000 раз без ограничений на число поколений. Для оценки их эффективности измерялось число вычислений функции приспособленности, что пропорционально времени генерации автомата. Приводимые ниже результаты относятся только к автомату управления дверьми лифта.

При этом использовалась спецификация, состоящая из девяти тестовых примеров, девяти позитивных сценариев, 30 негативных сценариев и 11 ¿/'¿-формул, из которых девять являются контрактами (пять инвариантов и четыре постусловия). При использовании только тестовых примеров построенный автомат в девяти случаях из 1000 соответствовал спецификации. Например, один из сгенерированных автоматов, мог после поломки лифта снова начать закрывать двери, что не соответствует спецификации. Также данный автомат мог повторно начать закрывать или открывать двери после их закрытия или открытия соответственно (рисунок 66).

5 I

е4 /

е11 /21

Л

3

е12/г2

б

Рисунок 6 - Две особи, построенные в ходе выполнения алгоритма генетического программирования

Результаты экспериментов приведены таблице. В ней не указаны результаты экспериментов только с тестовыми примерами, так как правильный автомат получался

только в I % случаев. Использование верификации позволяет строить автоматы, соответствующие спецификации всегда.

Таблица - Число вычислений функции приспособленности при генерации автомата управления дверьми лифта

Среднее значение Среднеквадратичное отклонение

Минимальное значение

Максимальное значение

Тесты и ¿7/,-формулы

8.372 ^ То'

7.57 х 10'

6.331 х кг

5.912 х ¡0"

1 есты, L /'/.-формулы и контракты

7.109 х ю5

6.32 х Ю

Сценарии, /. //.-формулы и контракты

1.616 х ю

1.102 х ¡о5

6.153 х ИТ 4.589 х К)"

3.808 х Ю4

8.162 х Ю

Полученные результаты позволяют утверждать, что применение сценариев позволило в 4-5 раз сократить время построения автомата управления дверьми лифта.

В третьей главе приводится сравнение трех подходов построения автоматных программ с использованием верификации. Первый построение автомата «вручную» и последующая верификация; второй - генетическое программирование по тестам; третий генетическое программирование по сценариям работы и контрактам с учетом верификации в функции приспособленности, операциях скрещивания и мутации.

Первые два подхода обладают недостатком - необходима дополнительная верификация, и при обнаружении ошибки необходимо вносить изменения в автомат. Третий подход лишен этого недостатка - он позволяет на выходе алгоритма генетического программирования получать автомат, соответствующий спецификации за счет того, что каждая особь, генерируемая алгоритмом, подвергается верификации. На базе этого подхода создана соответствующая технология (рисунок 7).

i Параметры ] эксперимента

Входные перчме'^ые / вЫпЛЦутс' ВОЗДеЙОВКЯ

Алгоритм генетического программирования, учитывающий верификацию в функции приспособленности, операциях мутации и скрещивания

'.....-j Набор тестов или

\ ,—( сценариев

1П1

I TL-формулы и контракты

ч

Управляющий конечный автомат

V___^

Рисунок 7 - Схема, соответствующая технологии генерации автоматов на основе генетического программирования и верификации

Предложенная технология реализована в инструментальном средстве GABP (Genetic Automata-Based Programming), которое доступно по адресу:

http://code.google.eom/p/gabp/. Это средство содержит верификатор Automata Veríftcator, упомянутый в главе 1. Инструментальное средство GABP принимает на вход ХМ1,-файл, содержащий параметры эксперимента и спецификацию. На выходе строится М//.-описание в формате инструментального средства UniMod (http://uninwd.sourceforge.net/), который позволяет генерировать код на языке Java или непосредственно исполнять сгенерированный автомат.

В четвертой главе приведены результаты внедрения разработанной технологии и предложенного инструментального средства для генерации соответствующего спецификации автомата для модуля Top Traffic Monitor, осуществляющего поиск узлов сети с максимальным трафиком, который входит в программный продукт NeíFlaw Integrator (http://netflovviogic.com), предназначенный для мониторинга сети и поиска потенциальных сетевых атак или угроз.

Каждый модуль для NetFlow Integrator описывается графом потока управления и данных (Control and Data Flow Graph, CDFG). Вершины этого графа выполняют операции над Л'е/Г/ои'-сообщениями, а ребра бывают двух типов: Control Flow (последовательность выполнения операций) и Data Flow (связь между источниками и приемниками данных). Граф может быть преобразован в автомат и наоборот. При этом для построения графа предлагается сгенерировать автомат с помощью разработанного средства и преобразовать его в граф.

При построении модуля использовалась спецификация из 10 позитивных сценариев, 27 негативных сценариев и девяти ¿TL-формул, из которых шесть -контракты. Автомат строился 1000 раз с помощью генетического программирования без ограничения на число поколений при следующих исходных данных: размер начальной популяции - 2000, число состояний автомата начального поколения-7, ожидаемое число переходов - 9, доля особей, переходящих в следующее поколение -10 %, вероятность мутации - 2 %.

Для оценки скорости работы алгоритма генетического программирования измерялось число вычислений функции приспособленности. Среднее значение -3.012 х 105. Среднеквадратичное отклонение— 1.904 х 105. Минимальное число вычислений -8.318 * 104. Максимачьное число - 2.096 * 106.

Автомат представлен на рисунке 8а, а граф - на рисунке

--tmpl/mc2

nfv5/mr1

s1

nfv5- - *

ч

nfv9/mr2

>; * ь

t

tmp'/mcl-

s3

t c2.end/c1 clean, c2.clean, k.reset

\ c2.next/c1 .exp f

s4 j/"

j ............ .end"'

, !

Vc1 exp/s!

/ \ "^e /.-. л

CÍ next X /, <2 next 4 1

\v / false \

Рисунок 8 - Модуль Top Traffic Monitor. Автомат (а) и граф (б)

Испытания программного продукта NetFlow Integrator показали, что построенный модуль работает правильно.

Заключение

В ходе диссертационной работы получены следующие результаты, обладающие научной новизной:

1. Предложена функция приспособленности, учитывающая верификацию. В отличие от известных, в ней вклад каждой 17Х-формулы не ноль или единица, а значение в интервале [0; 1], что более точно оценивает выполнение формулы.

2. Разработаны операции мутации и скрещивания, учитывающие верификацию, что позволяет строить конечный автомат быстрее, чем при учете верификации только в функции приспособленности.

3. Разработан алгоритм генерации автоматов с учетом контрактов. Ранее при генерации автоматов контракты не использовались. Так как контракты - это /^¿-формулы определенного вида, то их применение позволяет ускорить генерацию автоматов с учетом верификации.

4. Разработан алгоритм генерации автоматов по сценариям работы и верификации. Применение сценариев позволяет ускорить генерацию автоматов по сравнению с генерацией автоматов по тестам.

5. Разработан верификатор AutomataVerificator, приспособленный для поддержки генерации автоматов на основе генетического программирования.

6. Разработана технология генерации автоматов с помощью генетического программирования и верификации, которая не зависит от решаемой задачи.

7. На основе разработанных верификатора и технологии создано инструментальное средство САПР для генерации автоматов с помощью генетического программирования и верификации.

8. Это инструментальное средство было использовано для генерации автомата управления модулем Top Traffic Monitor для поиска узлов сети с максимальным трафиком, который входит в программный продукт NetFlow Integrator (ООО ЭВЕЛОПЕРС, Санкт-Петербург). Испытания этого продукта показали, что построенный автомат соответствует спецификации, а модуль работает правильно без дополнительной отладки.

Статьи в журналах из перечня ВАК

1. Егоров К. В., Шачыто А. А. Методика верификации автоматных программ // Информационно-управляющие системы. 2008. № 5, с. 15-21.

2. Егоров К. В., Шалыто А. А. Разработка верификатора автоматных программ //Научно-технический вестник СПбГУ ИТМО. 2008. Вып. 53. Автоматное программирование, с. 177-188.

3. Егоров К. В., Царев Ф. Я, Шалыто А. А. Применение генетического программирования для построения автоматов управления системами со сложным поведением на основе обучающих примеров и спецификации // Научно-технический вестник СПбГУ ИТМО. 2010. № 5 (69), с. 81 - 86.

Другие публикации

4. Егоров К, В., Царев Ф. Н. Совместное применение генетического программирования и верификации моделей для построения автоматов управления системами со сложным поведением / Сборник трудов 32-й конференция молодых ученых и специалистов «Информационные технологии и системы» (ИТИС-2009). М.: Институт проблем передачи информации им. А. А. Харкевича РАН. 2009, с. 77 - 82.

5. Егоров К. В., Царев Ф. Н., Парфенов В. Г. Совместное применение генетического программирования и верификации моделей для построения автоматов управления системами со сложным поведением /Труды XVII Всероссийской научно-методической конференции «Телематика-2010». Т. 2. СПбГУ ИТМО. 2010, с. 344, 345.

6. Егоров К. В., Царев Ф. К, Шалыто А. А. Совместное применение генетического программирования и верификации для построения автоматов управления системами со сложным поведением //Труды СПИИРАН. 2010. Вып. 15, с. 123 -135.

7. Егоров К. В., Царев Ф. Н. Применение генетического программирования для построения автоматов управления системами со сложным поведением на основе верификации моделей и обучающих примеров / Материалы второй межвузовской научной конференции по проблемам информатики «СПИССЖ-2011». СПб.: ВВМ. 2011, с. 343 - 350.

8. Егоров К. В., Шалыто А. А. Применение генетического программирования для построения автоматов управления системами со сложным поведением на основе контрактов и тестовых примеров /Материалы второй межвузовской научной конференции по проблемам информатики «СПИСОК-2011». СПб.: ВВМ. 2011, с. 351-355.

9. Егоров К. В., Шалыто А. А. Применение генетического программирования для построения автоматов управления системами со сложным поведением на основе контрактов и тестовых примеров / Сборник научных трудов VI-ой Международной научно-практической конференции «Интегрированные модели и мягкие вычисления в искусственном интеллекте. М.: Физмалит. 2011, с.610-615.

10. Egorov К., Tsarev F. Finite State Machine Induction using Genetic Programming Based on Testing and Model Checking / Proceedings of the 2011 GECCO Conference Companion on Genetic and Evolutionary Computation. NY: ACM. 2011, pp. 759 - 762.

И .Егоров К. В., Царев Ф.Н., Шалыто A.A. Построение автоматов управления системами со сложным поведением на основе верификации и сценариев работы / Материалы третьей всероссийской научной конференция по проблемам информатики «СПИСОК-2012». СПб.: ВВМ. СПбГУ. 2012, с. 411 - 414.

Тиражирование и брошюровка выполнены в учреждении «Университетские телекоммуникации»

197101, г. Санкт-Петербург, Саблинская ул., 14.

Тел (812) 233-46-69, объем 1,0 п.л.

Тираж 100 экз.

Санкт-Петербургский национальный исследовательский университет информационных технологий, механики и оптики

На правах рукописи

04201 453303

¿У

Егоров Кирилл Викторович

Генерация управляющих автоматов на основе генетического программирования и верификации

Специальность 05.13.11. Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

Диссертация на соискание ученой степени кандидата технических наук

Научный руководитель: доктор технических наук, профессор А. А. Шалыто

Санкт-Петербург - 2013 г.

ОГЛАВЛЕНИЕ

Введение...................................................................................................................5

Глава 1. Автоматное программирование и верификация автоматных программ.................................................................................................................16

1.1. Автоматное программирование.................................................................16

1.1.1. Технология автоматного программирования....................................17

1.1.2. Управляющий конечный автомат.......................................................20

1.2. Верификация автоматных программ........................................................21

1.2.1. Традиционная верификация моделей на основе метода

Model Checking...............................................................................................21

1.2.2. Особенности верификации автоматных программ..........................29

Выводы по главе 1.............................................................................................32

Глава 2. Применение генетического программирования и верификации для построения автоматов............................................................................................33

2.1. Модификация метода построение автоматов по темпоральным формулам и тестовым примерам......................................................................33

2.1.1. Входные и выходные данные.............................................................34

2.1.2. Особь алгоритма генетического программирования.......................35

2.1.3. Функция приспособленности.............................................................36

2.1.4. Мутация................................................................................................42

2.1.5. Скрещивание........................................................................................46

2.2. Модификации алгоритма построения автоматов на основе генетического программирования и верификации.........................................50

2.2.1. Построение автоматов по контрактам...............................................51

2.2.2. Сценарии работы.................................................................................55

2.3. Экспериментальные исследования...........................................................57

2.3.1. Автомат управления дверьми лифта..................................................59

2.3.2. Автомат управления часами с будильником.....................................74

Выводы по главе 2.............................................................................................87

Глава 3. Технология построения автоматных программ на основе генетического программирования и верификации.............................................89

3.1. Верификация автоматных программ и верификатор AutomataVerificator.............................................................................................89

3.2. Построение автоматных программ на основе генетического программирования по тестам...........................................................................92

3.3. Технология создания автоматных программ на основе генетического программирования и верификации..................................................................95

3.4. Инструментальное средство для поддержки технологии генерации автоматов на основе генетического программирования и верификации.....98

3.4.1. Использование инструментального средства.................................105

Выводы по главе 3...........................................................................................106

Глава 4. Внедрение результатов работы при построении модулей для программного продукта NetFlow Integrator......................................................107

4.1. Принцип работы приложения NetFlow Integrator.................................109

4.1.1. Правила обработки Afe/F/ow-сообщений.........................................110

4.1.2. Граф представления модуля..............................................................ИЗ

4.2. Построение модуля для NetFlow Integrator на основе генетического программирования и верификации................................................................115

4.2.1. Описание объектов управления.......................................................118

4.2.2. Входные и выходные воздействия...................................................119

4.2.3. Спецификация модуля.......................................................................121

4.2.4. Результаты построения модуля........................................................126

Выводы по главе 4...........................................................................................130

Заключение...........................................................................................................132

Список источников..............................................................................................134

Печатные издания на русском языке..............................................................134

Печатные издания на английском языке........................................................136

Ресурсы сети Интернет...................................................................................139

Публикации автора..........................................................................................141

Статьи в журналах из перечня ВАК...........................................................141

Другие статьи автора...................................................................................142

Материалы конференций с участием автора............................................142

Приложение 1. XML-описание данных для экспериментов по генерации

автомата управления дверьми лифта.................................................................144

Приложение 2. UniMod-модель автомата управления дверьми лифта...........147

Приложение 3. XML-описание данных для экспериментов по генерации

модуля Top traffic monitor....................................................................................148

Приложение 4. С/и/Мо^-модель автомата управления модулем Top traffic monitor...................................................................................................................151

ВВЕДЕНИЕ

Актуальность проблемы. Людям всегда хотелось уметь проверять правильность программ, но не просто убедиться, что программа правильно работает в конечном числе случаев, а уметь формально доказывать, что ее поведение соответствует спецификации. Метод проверки того, что программа соответствует заданной спецификации (обладает необходимыми свойствами) и называется верификацией [7]. На практике, полная верификация системы намного сложнее, чем ее создание. Поэтому верификация не всегда оправдана с точки зрения затрат, и проще исправлять ошибки по мере их обнаружения во время работы системы. Однако ошибки в некоторых системах могут обойтись слишком дорого. Например, в программах управления транспортом, медицинским оборудованием, военной техникой и другими объектами ошибки могут привести к гибели людей или большим финансовым потерям.

Проверке качества программного обеспечения (ПО) ответственных систем, казалось бы, должно было уделяться значительное внимание, но до недавнего времени это было не так, о чем свидетельствуют многочисленные аварии и сбои в системах.

Ошибка аппарата Ткегас-25 была, пожалуй, одной из самых дорогих ошибок в современной истории. Аппарат поступил в продажу в конце 1982 года, одиннадцать таких машин были установлены в Северной Америке (пять - в США и шесть - в Канаде). С июня 1985 по январь 1987 года ошибка в программной части привела к гибели троих пациентов из шести, получивших передозировку радиации [17].

За три года работы Ткегас-25 было обнаружено два программных дефекта [38]:

• логическая ошибка в обновлении параметров, когда оператор менял состояние аппарата;

о проверка безопасности не срабатывала, когда 8-битный счетчик переполнялся и достигал нуля каждые 256 итераций.

Такие ошибки, зависящие от скорости работы оператора, сложно обнаруживать и воспроизводить. Первый дефект возникал при выполнении двух условий [38]:

• оператору необходимо внести изменения одновременно в параметрах режима и уровня энергии;

• оператору необходимо успеть внести данные изменения в течение восьми секунд.

Возникновение второй ошибки завесило от случайности. Она воспроизводилось только тогда, когда клавиша нажималась в момент достижения нуля счетчиком, поэтому ее было практически невозможно обнаружить.

Другая программная ошибка привела к одной из самых дорогих катастроф, которая произошла 4.06.1996 года во время первого запуска новой ракеты-носителя Апап-5, разработанной Европейским космическим агентством. Запуск прошел неудачно - ракета самоуничтожилась через 37 секунд после старта из-за неверной работы бортового ПО [17].

Было установлено, что авария Апап-5 была вызвана необработанным исключением при преобразовании 64-битного значения с плавающей запятой в 16-битное целое значение со знаком [39].

К сожалению, отечественное освоение космоса также не обошлось без инцидентов, произошедших по вине ПО [53]. «В начале 70-х годов прошлого советскую марсианскую программу преследовали хронические неудачи. Из целой армады межпланетных станций только одной удалось совершить мягкую посадку, однако ни одной фотографии аппарат так и не передал. Оказывается, на аппараты марсианской серии впервые были установлены бортовые цифровые ЭВМ».

С каждым годом доля аппаратной части систем и устройств уменьшается, а программной увеличивается, как, например, это имеет место в автомобилях. Возрастающая сложность ПО приводит к увеличению числа ошибок. Для обеспечения корректности и надежности работы ответственных систем большое значение имеют различные методы тестирования и верификации, позволяющие выявлять ошибки на разных этапах разработки и сопровождения ПО.

На практике тестирование применяется в большинстве случаев. Однако оно позволяет находить ошибки, но не доказывает их отсутствие [26]. Правильность работы программы, используя данный подход, можно подтвердить только при конечном числе входных данных. Однако некоторые ошибки появляются крайне редко и сложно воспроизводятся. Поэтому, для того чтобы исключить возможность их появления, требуется рассмотреть практически все возможные варианты поведения системы.

Указанную проблему решает верификация - метод доказательства того, что программа соответствует спецификации. На практике часто используется метод, который называется верификацией на моделях {Model Checking). При этом спецификация задается в виде темпоральных формул, число которых в общем случае не известно. Поэтому соответствие программы спецификации может быть обеспечено, но это не будет доказательством правильности программы. При таком подходе используется логический формализм и математическое описание модели.

Процесс верификации разработанных программ делится на четыре части. Построение формальной модели по программе. Построение спецификации - формальная запись свойств, которые требуется проверить. Верификация - проверка выполнения спецификации на модели. Определения соответствия между ошибкой в модели и ошибкой в программе.

Сложность такого подхода заключается как в построении модели по программе, так и в самой верификации. Часто создание программы оказывается проще, чем ее проверка. Для вновь разрабатываемых программ целесообразно сначала построить модель, и только после верификации построить по ней программу.

Для автоматных программ [15], как для существующих, так и для вновь разрабатываемых, может быть применен один и тот же подход к верификации. Автоматная программа представляет собой модель, пригодную для верификации. Поэтому не требуется дополнительно преобразование программы в модель и определения соответствия между ошибкой в модели и в программе [9]. Модель автоматной программы представляет собой управляющий автомат или систему таких автоматов. Для автоматов этого класса характерно наличие событий, условий переходов, задаваемых булевыми формулами, и выходных воздействий, которые могут быть произвольными. В диссертации предполагается, что поведение программ задается одним автоматом, а при описании поведения системой автоматов, они могут быть представлены одним автоматом за счет их «произведения» [8].

Для многих задач автоматы удается строить эвристически, однако существуют задачи, для которых такое построение затруднительно или невозможно [23,24,31]. В рамках работ [18] был предложен подход к построению управляющих конечных автоматов (далее автоматов) по тестовым примерам на основе эволюционных алгоритмов. Его особенность состоит в том, что функция приспособленности и операции скрещивания и мутации не зависят от рассматриваемой задачи. При использовании такого подхода при создании автомата выделяются события {е1, е2, ...), входные переменные (х1, х2, ...) и выходные воздействия г2,...). В качестве тестов для автомата рассматривались пары последовательностей: первая описывает события и входные переменные, поступающие на вход автомата,

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

Особь эволюционного алгоритма представляет собой автомат, у которого не фиксированы выходные воздействия на переходах, а указано только их число. Для заполнения «скелета» автомата выходными воздействиями используется метод расстановки пометок [18]. После их расстановки вычисляется функция приспособленности, которая учитывает, насколько хорошо особь проходит тесты. Лучшие особи скрещиваются либо случайным образом, либо с сохранением той части автомата, на которой тесты выполняются. Процесс повторяется до тех пор, пока не появится особь, проходящая все тесты.

Предложенный подход обладает тем недостатком, что при построении неправильного (ошибочного) автомата пользователю приходится снова и снова модифицировать тесты или добавлять новые, пока не будет построен требуемый автомат. Такие действия могут занять много времени, так как построение сложного автомата эволюционными алгоритмами требует рассмотрения большого числа поколений [5, 10, 24]. Поэтому может оказаться, что построение автомата вручную займет меньше времени, чем использование эволюционного алгоритма.

В любом случае, даже построив кажущийся правильным и проходящий все тесты автомат, нельзя гарантировать его поведение при других входных воздействиях. Под правильностью подразумевается корректное поведение построенного автомата при любых возможных вариантах входных событий и входных переменных. Поэтому построение «всеобъемлющих» тестов практически невозможно.

Какие должны быть выходные воздействия при поступлении на вход автомата той последовательности событий, которая не была описана в тестах? Ответ на данный вопрос можно дать двумя способами. Первый — если автомат ведет себя неправильно при определенной

последовательности входных событий и переменных, то добавляется новый тест и автомат строится заново. Второй - использовать верификацию модели при построении автоматов.

Первый вариант плох тем, что приходится вручную искать ошибки в построенном автомате, и тем, что ошибка может быть не обнаружена, а второй — позволяет описывать бесконечное число вариантов поведения автомата. Второй подход используется в настоящей диссертации.

Известны всего несколько работ, в которых генетическое программирование применялось совместно с верификацией [32 - 37]. В них верификация учитывалась только в функции приспособленности, и вклад каждой темпоральной формулы был дискретен: ноль — формула не выполняется, единица - если она выполняется. Выбор начального поколения, мутации и скрещивания были случайны и не учитывали верификацию. В результате рост функции приспособленности следующего поколения был обусловлен только отбором особей, «проходящих» большее число темпоральных формул.

Существуют и другие работы, которые строят автоматы эволюционными алгоритмами [1, 12, 13, 31, 40, 41, 48 — 51], однако большинство из них решают определенную задачу или класс задач, не предлагая решения для общего случая.

Настоящая работа является развитием совместных работ автора и Ф.Н. Царева [19, 52, 69], в которых применялись эволюционные алгоритмы для построения автоматов по тестовым примерам и темпоральным формулам. В этих работах было предложено совместно применять тесты и темпоральные формулы. Результат верификации учитывался только в функции приспособленности, аналогично работам [32 - 37]. В работах [19, 52, 69] была предложена технология построения автоматов по тестам и темпоральным формулам. Основные отличия настоящей работы от предыдущих:

1. Вклад каждой темпоральной формулы в функцию приспособленности лежит на отрезке [0; 1], а не дискретен -ноль или единица. Это позволяет лучше учесть приспособленность особи.

2. Темпоральные формулы учитываются не только в функции приспособленности, но и при операциях скрещивания и мутации.

3. Предложен алгоритм генерации автоматов на основе генетического программирования с учетом контрактов, применение которых для автоматных программ было предложено в работе [2].

4. Предложен алгоритм генерации автоматов на основе генетического программирования по сценариям работы и верификации.

Цель работы - генерации автоматов на основе генетического программирования и верификации.

При этом задачи, решаемые в диссертации, состоят в следующем:

1. Предложить функцию приспособленности, учитывающую верификацию, проводимую в процессе выполнения алгоритма генетического программирования.

2. Разработать операции скрещивания и мутации, учитывающие верификацию.

3. Разработать алгоритм построения автоматов н