Поиск

Полнотекстовый поиск:
Где искать:
везде
только в названии
только в тексте
Выводить:
описание
слова в тексте
только заголовок

Рекомендуем ознакомиться

'Документ'
Грянувший в 2008-2009 гг. мировой экономический и финансовый кризис властно поставил в глобальную повестку дня проблему управляемости процессами миро...полностью>>
'Документ'
Санаторий расположен в 22 км от г. Адлер, в самом красивом районе Старой Гагры и находится на закрытой и охраняемой территории в красивом парке на сам...полностью>>
'Программа'
Математические и экономические предположения в моделях непрерывного времени. Процессы с непрерывными выборочными траекториями без редких событий. Про...полностью>>
'Конспект'
Хранение, накопление и поиск являются одними из основных действий, осуществляемых над информацией и главным средством обеспечения ее доступности в те...полностью>>

Министерство образования и науки российской федерации федеральное агентство по образованию (3)

Главная > Документ
Сохрани ссылку в одной из сетей:

МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ

Федеральное агентство по образованию

Государственное образовательное учреждение высшего профессионального образования

«Санкт-Петербургский государственный УНИВЕРСИТЕТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ, МЕХАНИКИ И ОПТИКИ»

Факультет Информационных технологий и программирования

Направление Прикладная математика и информатика

Специализация : Технологии программирования

Академическая степень магистр прикладной математики и информатики

Кафедра Компьютерных технологий Группа 6538

МАГИСТЕРСКАЯ ДИССЕРТАЦИЯ

на тему

Совместное применение генетического программирования и верификации моделей для построения автоматов управления системами со сложным поведением

Автор магистерской диссертации Егоров К.В. (подпись)

( Фамилия, И., О. )

Научный руководитель Шалыто А.А. (подпись)

( Фамилия, И., О. )

Руководитель магистерской программы________________________________(подпись)

( Фамилия, И., О. )

К з а щ и т е д о п у с т и т ь

Зав. кафедрой ВАСИЛЬЕВ В.Н. (подпись)

( Фамилия, И., О. )

“____”____________________20 ____г.

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

Магистерская диссертация выполнена с оценкой _______________________________

Дата защиты “____”________________________20____г.

Секретарь ГАК ____________________________________

Листов хранения ___________________________________

Чертежей хранения _________________________________

Санкт-Петербургский государственный университет

информационных технологий механики и оптики

АННОТАЦИЯ

ПО МАГИСТЕРСКОЙ ДИССЕРТАЦИИ

Студента Егоров К.В.

Факультет Информационных Технологий и Программирования

Кафедра Компьютерных технологий Группа 6538

Направление (специальность) Прикладная математика и информатика

Квалификация (степень) магистр прикладной математики и информатики

Наименование темы: Совместное применение генетического программирования и верификации моделей для построения автоматов управления системами со сложным поведением

Руководитель Шалыто А.А., доктор технических наук, профессор, заведующий кафедрой «Технологии программирования», СПб ГУ ИТМО

КРАТКОЕ СОДЕРЖАНИЕ МАГИСТЕРСКОЙ ДИССЕРТАЦИИ

И ОСНОВНЫЕ ВЫВОДЫ

объем 69 стр., графический материал - стр., библиография 16 наим.

Направление и задача исследований

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

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

Проектная или исследовательская часть (с указанием основных методов исследований, расчетов и результатов)

Исследовательская часть заключалась в изучении возможности применения верификации модели автоматной программы для автоматического ее создания. Требования к автоматной программе записываются на языке логики линейного времени (Linear Time Logic, LTL).

В предлагаемом методе применяется генетический алгоритм для создания автоматных программ. Исходными данными для алгоритма являются: набор тестовых примеров и набор темпоральных свойств (LTL‑формул). В качестве особи генетического алгоритма берется управляющий конечный автомат. При построении автомата, проходящего все тесты и удовлетворяющего всем свойствам, разработанное средство возвращает xml-описание модели в формате UniMod.

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

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

Экономическая часть (какие использованы методики, экономическая эффективность результатов)

Экономическая часть не исследовалась.

Характеристика вопросов экологии, техники безопасности и др.

Работа является программным продуктом и не связана с вопросами экологии и техники безопасности.

Является ли работа продолжением курсовых проектов (работ), есть ли публикации

Работа является продолжением работы Царева Ф.Н. Метод построения автоматов управления системами со сложным поведением на основе тестов с помощью генетического программирования / Материалы Международной научной конференции «Компьютерные науки и информационные технологии». Саратов: СГУ. 2009, с. 216–219

Публикации:

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

Практическая ценность работы. Рекомендации по внедрению

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

Содержание

Содержание 5

Введение 8

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

1.1. Язык логики линейного времени 13

1.2. Алгоритм верификации 14

1.3. Программная реализация верификатора 17

Выводы по главе 1 19

ГЛАВА 2. Описание предлагаемого метода 20

2.1. Представление конечного автомата в виде хромосомы генетического алгоритма 21

2.1.1. Обработка входных переменных 22

2.2. Вычисление функции приспособленности 23

2.2.1. Учет результата верификации при вычислении функции приспособленности 27

2.3. Операция мутации 28

2.4. Операция скрещивания 32

2.4.1. Скрещивание с учетом результата верификации 33

2.5. Методика построения автоматных программ 36

Выводы по главе 2 40

ГЛАВА 3. Программная реализация метода и экспериментальное исследование 41

3.1. Программная реализация 41

3.2. Построение конечного автомата управления часами с будильником 47

3.2.1. Система тестовых примеров и темпоральных свойств 49

3.2.2. Результаты применения генетического алгоритма 52

3.3. Построение конечного автомата управления дверьми лифта 58

3.3.1. Система тестовых примеров 59

3.3.2. Результаты эксперимента 63

Выводы по главе 3 67

Заключение 68

Источники 69

Введение

Автоматное программирование – это парадигма программирования, в рамках которой программы предлагается проектировать в виде совокупности взаимодействующих автоматизированных объектов управления [1]. В автоматных программах выделяют три типа объектов: поставщики событий, система управления и объекты управления. Система управления представляет собой конечный автомат или систему взаимодействующих конечных автоматов. Поставщики событий генерируют события, а система управления по каждому событию может совершать переход, считывая значения входных переменных у объектов управления для проверки условия перехода.

Для многих задач автоматы удается строить эвристически, однако существуют задачи, для которых такое построение затруднительно [2–4]. В рамках работы [5] был предложен подход к построению управляющих конечных автоматов на основе обучающих примеров. При использовании такого метода на начальном этапе проектирования автомата (модели) выделяются события (e1, e2, …), входные переменные (x1, x2, …) и выходные воздействия (z1, z2, …). В качестве тестов для управляющего конечного автомата рассматривались пары последовательностей, одна из которых описывает события и входные переменные, поступающие на вход автомату, а вторая – выходные воздействия, которые должен вырабатывать автомат при обработке этих событий.

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

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

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

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

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

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

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

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

Наиболее практичным в настоящее время является метод верификации, называемый Model Checking [6, 7]. При его использовании процесс верификации состоит из трех этапов. Первый из них, моделирование программы состоит в преобразовании программы в формальную модель с конечным числом состояний для последующей верификации.
Второй этап, спецификация – формальная запись утверждений, которые требуется проверить. На третьем этапе, выполняется собственно верификация – алгоритмическая проверка выполнения спецификации для модели.

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

  1. Стандартный процесс верификации программы

Однако, метод Model Checking достаточно хорошо подходит для случая автоматных программ, так как нет необходимости преобразовывать программу в модель, и после верификации, в случае обнаружения контрпримера, совершать обратное преобразование. Это объясняется тем, что автомат уже является моделью, пригодной для верификации, и не требует никаких дополнительных преобразований и упрощений. Такая особенность автоматов позволяет строить утверждения о программе в терминах автоматов, что упрощает их верификацию по сравнению с программами, написанными традиционным путем (без явного выделения состояний).

В предлагаемом методе будет проводиться верификация не всей автоматной программы, а только ее модель (конечный автомат). Это немного упрощает задачу, но так же, как и при создании автоматной программы на основе тестов, мы считаем поставщиков событий и объекты управления достаточно простыми, а вся сложная логика вынесена в автоматную модель. При верификации будем рассматривать поставщиков событий и объекты управления в качестве «внешней среды», которая ничего не помнит о последовательности переходов рассматриваемого автомата. Таким образом, в любой момент времени может быть получено любое событие, и любое условие на переходе может быть как истинным, так и ложным. Это приводит к тому, что автомат может совершить любой переход из данного состояния. Такой подход уже был рассмотрен в работе [8]. Но это не является упрощением модели в случае вынесения всей логики в автоматную.

В настоящей работе требования к программе формулируются в виде формул темпоральной логики линейного времени (Linear Temporal Logic, LTL). Далее кратко опишем синтаксис и семантику этого языка. Сразу заметим, что как выбор языка темпоральной логики, так и выбор верификатора не влияет на предложенный метод построения автоматных программ генетическими алгоритмами. Это позволяет применять его с другими программными средствами, реализующими верификацию методом Model Checking.

1.1.Язык логики линейного времени

Как уже отмечалось ранее, для описания поведения автомата будем применять утверждения, написанные на языке LTL. Синтаксис LTL включает в себя пропозициональные переменные Prop, булевы связки (¬, Λ, V) и темпоральные операторы. Последние применяются для составления утверждений о событиях в будущем и интерпретируются как I: Prop →.{True, False}.

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

Будем использовать следующие темпоральные операторы:

  • X (neXt) – «Xp» – в следующий момент выполнено p;

  • F (in the Future) – «Fp» – в некоторый момент в будущем будет выполнено p;

  • G (Globally in the future) – «Gp» – всегда в будущем выполняется p;

  • U (Until) – «pUq» – существует состояние, в котором выполнено q и во всех предыдущих выполняется p;

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

Множество LTL формул таково:

  • пропозициональные переменные Prop;

  • True, False;

  • φ и ψ – формулы, то

    • ¬φ, φΛψ, φVψ – формулы;

    • Xφ, Fφ, Gφ, φUψ, φRψ – формулы.

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

1.2.Алгоритм верификации

Алгоритм верификации основан на том, что как модель автоматной программы, так и LTL‑формулу можно представить в виде автомата Бюхи. Формально он определяется пятеркой (S, E, T, s0, F), где

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

  • E – множество меток переходов;

  • – множество переходов;

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

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

Тогда путь в этом графе π = s0, s1, s2, … sn, …, для которого выполнено T(si-1, e, si), где e – метка перехода, будет последовательностью вычислений системы. Путь является допускающим, если существует состояние из множества F, встречающееся бесконечно часто.

Подробно о трансляции LTL‑формулы в автомат Бюхи изложено в работах [7, 9, 10].

Приведем несколько примеров автоматов Бюхи, построенного по основным формулам. На Рис. 2. приведены автоматы, построенные для темпоральных операторов Future, Until и Release. Как «init» обозначены начальные состояния, а состояния, отмеченные двойным кругом, являются допускающими.

а

б

в

  1. Автоматы Бюхи, построенные для LTL‑формул
    Fp (а), pUq (б), pRq (в)

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

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

В связи с тем, что рассматриваются бесконечные слова, то, как доказано в работе [7], для пустоты пересечения достаточно доказать, что ни одно допускающее состояние не принадлежит сильной компоненте связанности, которая достижима из начального состояния (не существует цикла, проходящего через допускающее состояние). Таким образом, при нахождении цикла, достижимого из начального состояния, будет построен контрпример – путь в модели, на котором не выполняется LTL‑формула.

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

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

Приведем рекурсивный алгоритм двойного обхода в глубину на псевдокоде из работы [7].

procedure emptiness

for all q0 ϵ Q0 do

dfs1(q0);

terminate(False);

end procedure

procedure dfs1(q)

local q’;

hash(q);

for all последователей q’ вершины q do

if q’ не содержится в хэш-таблице then dfs1(q’);

if accept(q) then dfs2(q);

end procedure

procedure dfs2(q)

local q’;

flag(q);

for all последователей q’ вершины q do

if q’ в стеке dfs1 then terminate(True);

else if q’ не является помеченной then dfs2(q’);

end if;

end procedure

Приведенный алгоритм работает следующим образом: когда первый обход в глубину (Depth-first search, DFS) покидает состояние, он вызывает второй DFS для обнаружения циклов. Если второй DFS пришел в состояние, содержащееся в стеке первого DFS, то цикл найден. Тогда стек первого DFS содержит конечный префикс контрпримера, а второй обнаружил цикл, который служит бесконечным суффиксом. Таким образом, язык пересечения автоматов Бюхи не пуст.

1.3.Программная реализация верификатора

В настоящей работе использовался верификатор, реализованный в работе [11]. Верификатор на вход получает модель автоматной программы и LTL‑формулу. После проверки модели верификатор либо сообщает, что формула выполняется, либо приводит контрпример в виде последовательности состояний и переходов в конечном автомате (Рис. 3.).

  1. Схема работы верификатора

Как уже отмечалось выше, выбор верификатора и языка темпоральной логики не имеет значения, но использовалась именно эта реализация, так как этот верификатор написан на языке программирования Java и предназначен для проверки утверждений об автоматных программах. Верификатор предоставляет набор классов для трансляции LTL‑формул в автомат Бюхи и дальнейшей проверки пустоты языка пересечения отрицания LTL‑формулы и языка, допускаемого автоматом модели.

Верификатор из работы [11] реализует алгоритм двойного обхода в глубину, описанный выше. При этом, в случае обнаружения ошибки в модели и существования контрпримера, опровергающего утверждение о ней, данному алгоритму не требуется построение полного автомата пересечения двух автоматов Бюхи. Однако, в случае выполнимости формулы, полный автомат пересечения все-таки будет построен.

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

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

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

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

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

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

Однако в ряде случаев выразительности таких предикатов может не хватать для проверки утверждений, которые могут потребоваться. Поэтому используемый верификатор дает возможность создавать собственные предикаты. Это позволяет не строить «хитрые» утверждения, использующие стандартные предикаты и логические операторы. Например, для проверки утверждения «действие o1.z2 вызывается через одно после o1.z1» достаточно написать один метод на языке Java, которому доступна информация о совершенном переходе. Таким образом, можно легко проверять такого рода утверждения, не прибегая к сложной комбинации предопределенных предикатов.

При этом утверждения об автоматной программе записываются обычной строкой, например, «G(wasEvent(p1.e1))» или «F(wasAction(o1.z1))». Таким образом, синтаксис LTL‑формул остался таким же, как в разд. 1.1. Это позволяет записывать утверждения о программе человеку, который знает только синтаксис и семантику языка LTL.

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

В настоящем разделы было дано понятие верификации, описан язык логики линейного времени (LTL), дано описание и основная идея алгоритма верификации. Предлагаемый метод может использовать любой верификатор, позволяющий проверять утверждения об автоматных программах, но в работе использовался верификатор из работы [11].

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



Скачать документ

Похожие документы:

  1. Министерство образования и науки российской федерации федеральное агентство по образованию (6)

    Документ
    Конспект лекций содержит все основные разделы, предусмотренные программой учебного курса по праву интеллектуальной собственности и полностью соответствует государственному образовательному стандарту данной учебной дисциплины.
  2. Министерство образования и науки российской федерации федеральное агентство по образованию (2)

    Документ
    МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИФЕДЕРАЛЬНОЕ АГЕНТСТВО ПО ОБРАЗОВАНИЮГосударственное образовательное учреждение высшего профессионального образования
  3. Министерство образования и науки российской федерации федеральное агентство по образованию (4)

    Документ
    Публикуемая работа представляет собой аналитический доклад промежуточного отчета за I полугодие 2006 г. по проекту «Исследование основных тенденций развития и терминологической базы Болонского процесса как структурной реформы высшего
  4. Министерство образования и науки Российской Федерации Федеральное агентство по образованию (1)

    Документ
    Конференция проводится с целью стимулирования научно-технической деятельности молодых учёных, приобретения ими опыта публичных выступлений и подачи научных документов для публикации, а также с целью ознакомления научной общественности с результатами
  5. Министерство образования и науки Российской Федерации Федеральное агентство по образованию (7)

    Документ
    Конференция проводится с целью стимулирования научно-технической деятельности молодых учёных, приобретения ими опыта публичных выступлений и подачи научных документов для публикации, а также с целью ознакомления научной общественности с результатами
  6. Министерство образования и науки Российской Федерации Федеральное агентство по образованию (5)

    Реферат
    Настоящий литературный обзор предназначен для того, что сориентировать студента, обучающегося по программе МИГО, относительно круга проблем в области междисцилинарных исследований в юриспруденции.

Другие похожие документы..