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

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

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

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


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


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


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

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

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


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


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


на тему


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


Автор магистерской диссертации^ Егоров К. Содержание
Содержание 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..



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

Однако, метод ^ 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» обозначены начальные состояния, а состояния, отмеченные двойным кругом, являются допускающими.







а

б

в

Автоматы Бюхи, построенные для 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.).



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

Как уже отмечалось выше, выбор верификатора и языка темпоральной логики не имеет значения, но использовалась именно эта реализация, так как этот верификатор написан на языке программирования 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 и верифицироваться верификатором, описанным в настоящем разделе.
^ ГЛАВА 2.Описание предлагаемого метода
Исходными данными для построения конечного автомата управления системой со сложным поведением являются:

список событий;

список входных переменных;

список выходных воздействий;

набор тестов, каждый из которых содержит последовательность Input[i] событий, поступающих на вход конечному автомату, и соответствующую ей эталонную последовательность Answer[i] выходных воздействий;

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

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

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

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

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

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



Некоторые переходы «скелета» автомата

В настоящей работе генетический алгоритм остался таким же, как и в работе [5], то есть он имеет все те же стадии: создание начальной популяции, вычисление функции приспособленности, скрещивание, мутация. Также сохранилась стратегия эллитизма. Однако предлагается учитывать результат верификации при вычислении функции приспособленности и мутации, о чем будет написано ниже. Для начала отметим отличие в обработки входных переменных при генерации на основе тестов и при верификации.
^ 2.1.1.Обработка входных переменных
Каждый переход может иметь условие, при котором он совершается. Такое условие записывается в виде логической формулы, которая задает ограничения на значения входных переменных. Например, можно записывать «T [!x1 && x2]», что означает, что переход совершится по событию T при условии невыполнимости x1 и выполнимости x2. При создании автоматной модели только на основе тестов, такой переход считается отличным от перехода просто по событию T без всяких условий – можно считать, что это два разных события.

Однако, оба перехода идентичны для предиката wasEvent(T) («переход совершен по событию Т»). При верификации, если переход был совершен по событию T или этому же событию, но с некоторыми условиями, то в обоих случаях данный предикат, естественно, будет выполнен. Заметим, что можно вводить предикаты и на условия на переходах, тогда такие переходы будут отличаться и для верификатора. Например, можно добавить предикат wasTrue(x1) (условие x1 верно), тогда он не будет выполняться на переходе «T [!x1 && x2]», но будет верен для перехода «T [x1 && x2]».
^ 2.2.Вычисление функции приспособленности
В любом генетическом алгоритме ключевую роль играет вычисление функции приспособленности. Она позволяет количественно оценивать особи: чем больше функция приспособленности, тем лучше особь. Таким образом, независимо от выбора стратегии генетического алгоритма, функция приспособленности лучшей особи в популяции, как правило, должна расти. В любом случае поиск автоматной модели считается завершенным, когда найдена особь, для которой значение функции приспособленности превышает некоторое целевой значение, заданное заранее.

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

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

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

Напомним, что функция приспособленности для тестов основана на редакционном расстоянии (расстоянии Левенштейна) [12]. Для ее вычисления выполняются следующие действия: на вход автомату подается каждая из последовательностей Input[i]. Обозначим последовательность выходных воздействий, которую сгенерировал автомат на входе Input[i] как Output[i]. После этого вычисляется величина , где как ED(A, B) обозначено редакционное расстояние между строками A и B. Отметим, что значения этой функции лежат в пределах от 0 до 1, при этом, чем «лучше» автомат соответствует тестам, тем больше значение функции приспособленности.

Для того чтобы выделять особи, проходящие все тесты, и те, которые проходят только часть, предлагалось вычислять функцию приспособленности для тестов по формуле: , где T – «стоимость» прохождения всех тестов.

Вклад LTL формул в общую функцию приспособленности предлагается оценивать как доля верных формул рассматриваемой особи. Этот вклад можно оценить как , где F – «стоимость» выполнения всех формул, n1 – число успешно выполненных LTL формул, а n2 – общее число формул. Таким образом, чем больше число верных формул, тем больше вклад теморальных свойств в функцию приспособленности, а, при выполнимости всех свойств, их вклад становится равным F.

Функция приспособленности зависит не только от того, насколько «хорошо» автомат работает на тестах и удовлетворяет формулам, но и числа переходов, которые он содержит. Таким образов, функцию приспособленности можно вычислить по формуле: , где как cnt обозначено число переходов в автомате, C – число, больше чем число переходов, а FFtest и FFLTL – вклады тестов и формул соответственно. Эта функция приспособленности устроена таким образом, что при одинаковом значении FFtest + FFLTL, отражающем «прохождение» тестов и LTL формул автоматом, преимущество имеет модель, содержащая меньше переходов.

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

Также в настоящей работе предлагается не вычислять функцию приспособленности для всех тестов и формул одновременно, а разбивать их на группы и вычислять для каждой группы отдельно. Каждая такая группа включает набор тестов и набор LTL формул, которые описывают определенное поведение модели, а значит особь, которая полностью проходит все тесты конкретной функциональности и удовлетворяет всем ее темпоральным свойствам, будет лучше, чем особь, проходящая только часть тестов из разных групп. Тогда можно записать функцию приспособленности следующим образом: , где FFtest,i и FFLTL,i – функции приспособленности для тестов и для темпоральных свойств, вычисленные для i ой группы, а как N обозначено число групп. Вычисление функций приспособленности для каждой группы выполняется так же, как описано выше.

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

Оценить время верификации одной ^ LTL формулы можно только примерно. Если n – длина формулы, то в худшем случае будет построен автомат Бюхи с n × 2n состояниями [13]. Значит, автомат-пересечение будет содержать n × 2n × V состояний, где V – число вершин в модели. Заметим, что верификатор использует средство LTL2BA [14] для построения автомата Бюхи по LTL формуле, которое преобразует формулу перед построением автомата и модифицирует автомат после. В итоге построенный автомат не будет экспоненциально расти от длины формулы. Как правило, верифицируемые формулы достаточно компактные, что не будет приводить к автоматам с большим числом состояний.

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

Также заметим, что при верификации не всегда требуется целиком обходить автомат пересечения. Если модель не удовлетворяет темпоральному свойству, то контрпример может быть найден задолго до обхода всего автомата. Но даже, когда формула выполняется, автомат пересечения может быть меньше, чем n × 2n × V, так как многие вершины могут оказаться недостижимы.

Из сказанного следует, что процесс верификации может занимать много времени и, чем больше формул мы хотим использовать при построении автомата, тем дольше будет вычисляться функция приспособленности конкретной особи. Так как в каждом поколении могут быть тысячи особей, то выбор верификатора и его эффективность в плане производительности крайне важны.
^ 2.2.1.Учет результата верификации при вычислении функции приспособленности
Вклад каждого теста оценивается по редакционному расстоянию между эталонной выходной последовательностью и выходной последовательностью, сгенерированной особью. Тем самым, каждый тест вносит не просто «0» или «1», показывая, что тест пройден на конечном автомате или нет, а некоторое вещественное число из отрезка [0; 1] (оба конца включительно).

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

Предлагается в качестве вклада LTL формул в функцию приспособленности брать отношение числа проверенных переходов к числу достижимых переходов. Формулу можно записать как , где n – число LTL формул, T – число достижимых переходов в особи, ti – число переходов, помеченных как проверенные при верифкации i-ой формулы. Чем больше переходов было отмечено в процессе верификации, тем больше вклад формулы в функцию приспособленности, а значит и особь является более приспособленной.

Приведем пример вычисления вклада одной из LTL формул. Пусть мы верифицируем конечный автомат из шести состояний, представленный на Рис. 5.. Цифрой «1» выделена часть автомата, на которой не удалось обнаружить контрпример, а цифрой «2» – часть автомата, на которой формула опровергается.



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

Таким образом, вклад данной формулы будет , где 3 – число помеченных переходов из первого подмножества, а 7 – общее число переходов в конечном автомате.

Заметим, что порядок обхода в глубину состояний и переходов автомата не гарантируется, поэтому могло получиться так, что контрпример (помеченный цифрой 2 на Рис. 5.) мог быть найден сразу. Тогда вклад формулы в функцию приспособленности оказался бы нулевым, так как ни один из переходов не был бы помечен.
^ 2.3.Операция мутации
Выполнимость или невыполнимость LTL формул позволяет только отбирать «лучшие» особи, но не позволяет «улучшать» популяцию путем скрещивания или мутации, так как этот процесс был бы случайным и не гарантировал бы увеличения числа верных утверждений в следующем поколении. То есть, учитывая только относительное число выполненных темпоральных свойств, мы не можем влиять на результат скрещивания или мутации, однако именно эти операции и приводят к росту значения функции приспособленности.

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

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

при копировании перехода в новую особь с некоторой вероятностью у него одновременно меняются: входное событие, число выходных воздействий и конечное состояние;

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

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

Мы не можем автоматически проанализировать семантику формулы и понять, как надо исправить переход, чтобы формула стала выполняться. Поэтому одновременно меняется входное событие, число выходных воздействий и конечное состояние перехода, так как мы не знаем, какой из предикатов в LTL формуле выполняется или не выполняется на данном пути. Предикат может «говорить» о событии, может «говорить» о вызванном действии, а, может быть, рассматриваемый переход ведет в состояние, для которого некоторая подформула LTL-формулы является неверной.

Приведем пример верификации модели и операции мутации. Пусть одна из особей в поколении оказалась такой, как представлена на Рис. 6..



Пример конечного автомата

Пусть необходимо проверить утверждение «G(!wasEvent(T))», которое означает, что никогда не будет обработано событ