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

Павлова Елена Анатольевна

МЕТОДЫ И ПРОГРАММНЫЕ СРЕДСТВА РАЗРАБОТКИ ЛОГИЧЕСКИХ КОМПОНЕНТОВ СИСТЕМ С ПОШАГОВЫМИ

СТРАТЕГИЯМИ

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

АВТОРЕФЕРАТ

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

Автор: _

2 ИЮН 2011

Москва-2011

4848902

Работа выполнена в Национальном исследовательском ядерном университете «МИФИ» (НИЯУ МИФИ)

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

кандидат технических наук, доцент Сергиевский Максим Владимирович

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

доктор технических наук, профессор Косяченко Станислав Анатольевич

кандидат технических наук, доцент Серов Владимир Александрович

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

Институт Системного Программирования Российской Академии Наук

Защита состоится 30 июня 2011 г. В 15 часов 00 минут на заседании диссертационного совета Д 212.130.03 при Национальном исследовательском ядерном университете «МИФИ» по адресу: 115409, г. Москва, Каширское ш., 31. Тел. для справок: +7 (495) 323-95-26.

С диссертацией можно ознакомиться в библиотеке Национального исследовательского ядерного университета «МИФИ» (НИЯУ МИФИ).

Отзывы в двух экземплярах, заверенные печатью, просьба направлять по адресу: 115409, г. Москва, Каширское ш., д.31, отдел диссертационных советов НИЯУ МИФИ, тел.:+7 (495) 323-95-26.

Автореферат разослан « 26 » мая 2011 г.

Ученый секретарь

диссертационного совета

Леонова Н.М.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

Логический компонент (logic engine) - компонент, инкапсулирующий правила и предоставляющий интерфейс, содержащий методы определения изменений состояния системы в результате действий пользователей. В настоящей работе рассматриваются системы с пошаговыми стратегиями, в частности программы-тренажеры и игры. Термин "пошаговая" означает, что функционирование системы может быть описано с помощью упорядоченных во времени процессов, называемых ходами. Смысл работы системы заключается в эффективном управлении некоторыми ресурсами, используя которые, необходимо добиться определенного результата, например, преимущества над противником. Обязательным является наличие оперативного плана, разрабатываемого с учётом меняющейся обстановки. Обычными ресурсами в военных стратегиях являются войска (отдельные персонажи, подразделения или армии) и позиция, которые следует развивать и использовать для достижения преимущества. В экономических стратегиях акцент ставится на развитие экономической инфраструктуры, подконтрольной одной из сторон. Современные системы с пошаговыми стратегиями, как правило, соединяют в себе как военные, так и экономические факторы.

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

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

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

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

Традиционными языками разработчиков систем с пошаговыми стратегиями являются С и С++, кроме того, часто используются ассемблерные вставки. В связи с этим, реализация часто выполняется в среде разработки Microsoft Visual Studio. При реализации логического компонента и определении структур данных разработчики анализируют описания правил. Поскольку чаще всего используется неформальное описание Правил, процесс реализации логического компонента требует значительных

усилий и ресурсов, затруднена генерация кода на основе правил.

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

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

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

Объектом исследования диссертационной работы являются системы с пошаговыми стратегиями.

Предмет исследования диссертационной работы - разработка логических компонентов систем с пошаговыми стратегиями.

Целью диссертационной работы является создание метода разработки логических компонентов систем с пошаговыми стратегиями и разработка

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

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

• анализ существующих методов и инструментальных средств для проектирования, реализации и верификации логических компонентов систем с пошаговыми стратегиями;

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

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

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

• проектирование архитектуры системы поддержки разработки логических компонентов систем с пошаговыми стратегиями;

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

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

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

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

• новый формальный язык для описания правил систем с пошаговыми стратегиями;

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

• новый алгоритм статической проверки свойств совместности;

• новый алгоритм сокращения числа состояний для верификации свойств сбалансированности при помощи проверки на модели (model checking).

Практическая значимость результатов определяется следующим:

• реализован язык для описания правил систем с пошаговыми стратегиями. Язык учитывает особенности таких систем и позволяет проектировщику правил создавать графические описания правил в терминах предметной области;

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

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

Результаты работы могут быть использованы при решении задач разработки эенажёров, компьютерных игр, обучающих программ и других интерактивных >афических сред.

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

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

• на Научной сессии МИФИ в 2008 г.;

• на V Всероссийской конференции студентов, аспирантов и молодых ученых «Технологии Microsoft в теории и практике программирования» в 2008 г.;

• на Software Engineering Conference (Russia), SEC(R) в 2008 г.;

• на Научной сессии МИФИ в 2009 г.;

• на VI Всероссийской конференции студентов, аспирантов и молодых ученых «Технологии Microsoft в теории и практике программирования» в 2009 г.;

• на Third Spring Young Researchers' Colloquium on Software Engineering SYRCoSE) в 2009 г.;

• на научном семинаре ИСП РАН в 2009 г.;

• на Научной сессии МИФИ в 2010 г. Основные положения, выносимые на защиту:

• результаты анализа методов проектирования, верификации и реализации огических компонентов систем с пошаговыми стратегиями;

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

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

о алгоритм верификации совместности правил систем с пошаговыми стратегиями;

о алгоритм сокращения числа состояний для верификации свойств сбалансированности при помощи проверки на модели (model checking);

• архитектура системы поддержки разработки логических компонентов систем с пошаговыми стратегиями;

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

Структура работы. Работа состоит из введения, четырёх глав, заключения, списка литературы, включающего 144 наименования, и семи приложений. Текст диссертации изложен на 165 страницах, включая 39 рисунков и 18 таблиц.

СОДЕРЖАНИЕ РАБОТЫ

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

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

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

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

Рассмотрим традиционный подход к разработке логических компонентов, представление о котором можно составить по описанию отдельных особенностей подхода в исследовательской литературе. Подход включает следующие действия: анализ предметной области, проектирование правил, их реализацию и тестирование. Проектирование правил систем с пошаговыми стратегиями осуществляет проектировщик правил. Результатом проектирования является текстовый документ на естественном языке и сопровождающие его таблицы. Документ содержит подробное описание правил, а таблицы представляют свод численных характеристик объектов. Текстовый документ не имеет чётко регламентированной структуры. Он создаётся при помощи текстового процессора, а таблицы - при помощи процессора электронных таблиц.

Реализацию выполняет команда разработчиков. Традиционными языками разработки являются С и С++. В связи с вышесказанным, реализация часто выполняется при помощи среды разработки Microsoft Visual Studio. Тестирование выполняется командой тестировщиков, которая может быть набрана из числа пользователей игры или программы-тренажёра. Тестирование отдельных свойств (например, сбалансированности правил) может выполняться проектировщиком правил путём тщательного просмотра проектной документации. В отдельных работах предлагается отложить тестирование на этап, следующий за выпуском продукта. Для автоматизации разработки логических компонентов применяются инструментальные

редства поддержки разработки (например, Torque Engine Advanced, FPS Creator, JeoAxis Engine, Offset Engine, Unreal Engine и C4 Engine). Отметим основные едостатки этих средств: многие инструменты не поддерживают графическое писание правил, описание совмещается с описанием графической составляющей и лементов искусственного интеллекта, не учитываются особенности конкретных истем. В частности, не существует средства, учитывающего специфику пошаговых тратегий. Многие инструменты не поддерживают автоматизированную проверку равил и не позволяют автоматизировать процесс создания прототипа программы на снове описания правил.

Методы проверки свойств совместности правил и баланса между пользователями наименее исследованы. Они могут быть проверены формальными методами, гарантирующими выполнение свойств в случае успешного завершения проверки. Наиболее перспективным методом проверки представляется сочетание статического анализа свойств совместности и верификации при помощи проверки на модели (model checking) для свойств баланса. Такой подход позволит проводить проверку в автоматизированном режиме и гарантировать выполнение или отсутствие определённых свойств. В качестве инструментального средства для проверки на модели предлагается использовать верификатор SPIN, позволяющий проводить параллельную верификацию модели на нескольких компьютерах, реализующий основные алгоритмы проверки на модели и подходы, связанные с сокращением числа состояний проверяемой модели. Для этого инструмента существует подробная документация и множество описаний примеров использования в исследовательских работах.

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

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

Далее подробно рассматривается язык описания правил пошаговых стратегий. Язык позволяет описывать объекты правил (включая их данные и поведение), отношения между объектами, реакцию одних объектов на поведение других. Синтаксис языка задаётся формальной грамматикой. Язык принадлежит к классу LL(1). Семантика языка задаётся в виде денотационной семантики, где конструкциям языка ставятся в соответствие выражения в ^-исчислении (исчисление объектов,

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

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

i.j и

где I"4 - требуемый интерфейс i-ro объекта для взаимодействия с j-м, Ц'-предоставляемый интерфейс i-ro объекта для взаимодействия с j-м. Модель семантически совместна тогда и только тогда, когда семантически совместны все пары взаимодействующих объектов модели:

V object,, object, :(£>,(/"',//') = True) & (Д (//V/*) = True). (2)

Пара взаимодействующих объектов objects и objectj совместна тогда и только тогда, когда допустим контракт предоставляемого для j-ro объекта интерфейса i-ro, и требуемого от i-ro интерфейса j-ro, и допустим контракт предоставляемого для i-ro интерфейса j-ro, и требуемого от j-ro интерфейса i-ro. Контракт предоставляемого и требуемого интерфейсов допустим (D,(Ireq,Ipr) = True) тогда и только тогда, когда для любого метода Ш/ из требуемого интерфейса Г4 найдётся метод т2 предоставляемого интерфейса f такой, что контракт этих методов является допустимым:

(D/(7"Vi') = 7hie)c> Vim, еГ" 3 m2elpr :DJmt,m1) = True. (3)

Контракт двух методов mi и т2 полагается допустимым тогда и только тогда, когда совпадают сигнатуры методов, из предусловия т2 следует предусловие mi, am постусловия mi следует постусловие т2: (£>„(«, ,т2) = True) о {(Qpredl => QpndX) & (R^ => Rposll) = Тгие)&(щ =m2), (4)

где Qpredi - предусловие метода mh Qpred2 - предусловие метода m2, Rposl, -постусловие метода от/,Rpostг ~ постусловие метода т2.

Ниже приводится предложенный в работе алгоритм проверки свойств совместности правил игр и программ-тренажёров класса пошаговых стратегий.

Шаг 1. Определить для каждого объекта модели правил предоставляемый интерфейс.

Шаг 2. Определить для каждого объекта требуемые интерфейсы.

Шаг 3. Проверить синтаксическую совместность модели при помощи шагов 3.13.3.

Шаг 3.1. Построить сумму ^ Ц' всех предоставляемых интерфейсов модели.

и

Шаг 3.2. Построить сумму ^ 1'р всех требуемых интерфейсов модели.

i.j

Шаг 3.3. Если выполняется ^ I'f с , модель синтаксически совместна,

i.j и

перейти к шагу 4, иначе модель синтаксически несовместна, перейти к шагу 6. Шаг 4. Проверить семантическую совместность модели правил игры. Для этого для всех пар взаимодействующих объектов А и В модели проверить допустимость контрактов требуемых и предоставляемых интерфейсов

(D, (I/"1,1/') = True) и (D: (//" ,1/') = True). Если модель семантически совместна, перейти к шагу 6, иначе перейти к шагу 5. Шаг 5. Модель правил несовместна. Шаг 6. Конец.

Рассмотрим ещё один вид свойств, которым должны обладать правила -свойство баланса между игроками. Формализуем наиболее часто используемые в литературе критерии баланса. Правила, не допускающие выигрыша одного из игроков, считаются несбалансированными. Свойство «игру может выиграть i-й игрок» формулируется в логике CTL следующим образом: EF (win=i), где i- переменная, в которой хранится номер игрока, win - переменная, содержащая номер победителя или О, если игра не окончена. В LTL-логике возможно выразить отрицание этого свойства:

EF(win = i) = A\(F(win = /)). (5)

Несбалансированными считаются правила, при которых i-й игрок всегда проигрывает за первые b ходов. Сформулируем отрицание критерия «Существуют варианты игры, в которых i-й игрок не проигрывает за первые b ходов», count — счётчик ходов, loose - номер проигравшего игрока:

EF((loosel = i) & (count < b)) = A \(F((loose! = i) & (count < b))). (6)

Считать несбалансированными правила, при которых состояние i-ro игрока всегда хуже или равно состоянию j-ro на протяжении первых b ходов:

EF((v,>Vj)& (count <b)) = A\(F((Vi > v,) & (count й b))), (7)

где vnVj- оценки состояния игроков на момент конкретного хода. Несбалансированны правила, при которых состояние i-ro игрока ухудшается на протяжении первых b ходов, deltavt - приращение состояния i-ro игрока за один ход: EF((deltavt > 0) & (count < b)) = A\(F((deltavi > 0) & (count й b))). (8)

Несправедливыми будем считать правила, когда отношение ущерба damageп наносимого отрядом i, к его оценочной стоимости pricet отличается более чем в b раз от отношения damageнаносимого отрядом j, к его оценочной стоимости pricet:

.J damage, damage (9)

A(j -L =---0 .

; pricet price j

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

Аналогичное свойство можно сформулировать в логике CTL :

AG(AF(win! = i) /), (10)

где f- счётчик ошибок. То есть, пока игрок не ошибся хотя бы один раз, он не проиграл.

Можно формулировать близкое по смыслу свойство в логике LTL:

AG(lfR [(loose)). (11)

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

В третьей главе рассматривается проектирование инструментального средства, основанного на предложенном методе разработке. На рисунке 1 приведена общая архитектура инструментального средства поддержки разработки логических компонентов систем с пошаговыми стратегиями. На концептуальном уровне проектирования формулируются требования, разрабатываются варианты использования инструмента и создаётся его концептуальная архитектура. При проектировании архитектуры логического уровня происходит предварительное определение высокоуровневых компонентов инструмента, построение диаграмм последовательностей для компонентов, определение основных классов инструмента и отношений между ними. На физическом уровне проектирования уточняются диаграммы классов, определяются атрибуты классов и их типы, а также методы классов. Классы распределяются по компонентам, уточняется компонентная архитектура, проектируется модель развёртывания. Диаграммы вариантов использования, последовательностей, диаграммы классов, компонентов и диаграммы развёртывания описаны на основе стандарта UML 2.0 в инструментальном средстве IBM Rational Suite.

Графический интерфейс :

Редактор правил

Панель Ef] инструментов языка

Редактор if] модели правил

Редактор g] свойств элементов правил

Предоставляет модель правил

Редактор конфигураций

Панель инструментов

Редактор карты

Редактор g] начальных условии

Редактор свойств g~] элементов конфигурации

Редактор параметров верификации

Предоставляет модели

Предостат лет параметры eept фикации

Преобразование и верификация;

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

Анализатор правил 3

Предост э вляет

модепидля

Генератор прототипа

JL

вери$

I кации

Генератор модели с

сокращённым числом состояний для верификации

1L

Верификатор g]

Верификатор S совместности

Верификатор QJ сбалансированности

Предоставляет модели, код

Предоставляет результаты верификации

Хранилище данных

Правила; начальные конфигурации, результаты верификации, код прототипов

Рисунок 1 - Компонентная архитектура разработанного инструментального средства (в нотации UML 2.2)

В четвёртой главе рассматриваются особенности реализации и тестирования инструментального средства поддержки разработки логических компонентов. Реализация языка описания правил, спроектированного во второй главе, выполнена при помощи инструментального средства Visual Studio Domain-Specific Language Tools (далее DSL Tools). Для этого была построена графическая модель языка, содержащая элементы ядра языка и отношения между ними. На основе модели языка при помощи DSL Tools было сгенерировано приложение с графическим интерфейсом пользователя, способное интегрироваться в рабочую среду Visual Studio. Приложение содержит

редактор правил и конфигураций. Для генерации кода логического компонента были определены правила трансляции модели на разработанном языке в код на языке С#. При помощи DSL Tools на основе правил трансляции был реализован генератор прототипа, объединяющий сгенерированный на основе правил логический компонент и другие компоненты, входящие в состав систем с пошаговыми стратегиями.

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

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

Было проведено сравнение разработанного инструментального средства с системами, решающими аналогичные задачи, на основе критериев определённых во второй главе. Основными преимуществами инструментального средства являются: отделение описания правил от графического представления, возможность автоматической верификации игр, в том числе сбалансированности правил, и учёт специфики игр в классе пошаговых стратегий. Было проведено испытание разработанного инструментального средства на примере компьютерной программы-тренажёра TacOps 4, используемого более десяти лет вооруженными силами Канады, Австралии, Новой Зеландии, США и Германии. В результате верификации построенной для правил тренажёра модели при помощи инструментального средства было обнаружено нарушение свойства сбалансированности (4) для исходных правил, а также свойств (1) и (2) для модифицированных правил.

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

ОСНОВНЫЕ ВЫВОДЫ И РЕЗУЛЬТАТЫ РАБОТЫ 1. проведен анализ существующих методов разработки систем с пошаговыми стратегиями, представленных в публикациях. В частности, исследованы методы проектирования правил и методы обеспечения качества логических компонентов. На основе результатов анализа сделан вывод о недостаточности обеспечиваемого этими методами уровня качества логических компонентов и необходимости синтеза нового

метода разработки;

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

3. разработан новый язык описания правил систем с пошаговмих стратегиями. Язык учитывает особенности систем этого класса и позволяет проектировщику правил создавать графические описания правил в терминах предметной области;

4. для языка разработана формальная спецификация, определяющая синтаксис и денотационную семантику языка. Спецификация позволяет применить формальные методы анализа к описаниям правил на этом языке;

5. формализованы свойства, которым должны удовлетворять правила. Разработан новый алгоритм верификации свойств совместности при помощи статического анализа и новый алгоритм сокращения числа состояний для верификации свойств сбалансированности при помощи проверки на модели (model checking). Предложенные алгоритмы позволяют автоматизировать проверку сформулированных свойств;

6. разработана архитектура системы поддержки разработки логических компонентов систем с пошаговыми стратегиями. Система поддерживает разработку логических компонентов при помощи предложенного метода и создание на базе этого компонента исполнимого прототипа программы;

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

Основные публикации по теме диссертации:

Основные положения диссертационной работы опубликованы в 13 печатных трудах, в том числе в 4 статьях в журналах, включенных ВАК РФ в перечень ведущих рецензируемых научных журналов и изданий:

1. Гаврилов A.B., Павлова Б. А. Формализация проектирования сложных информационных систем на основе анализа функциональных интерфейсов // Информационные технологии №9, 2008. - М.: Новые технологии, 2008, с. 9-15. (Перечень ВАК)

2. Павлова £.А. Проектирование формального предметно-ориентированного языка (DSL) для разработки правил компьютерных игр в классе пошаговых стратегий // Вестник компьютерных и информационных технологий №4,2009 - М.: Машиностроение, 2009. - с. 45-52. (Перечень ВАК)

3.Павлова Е.А., Станкевичус A.A. Исследование сложности верификации моделей для правил логических компонентов с учётом свойств безопасности //

Безопасность информационных технологий. - М., 2009, №4. - с. 126-129. (Перечень ВАК)

4. Павлова Е.А. Автоматизация разработки правил компьютерных игр в классе пошаговых стратегий // Вестник компьютерных и информационных технологий №3,2010 - М.: Машиностроение, 2010. - с. 45-52. (Перечень ВАК)

5. Гаврилов А.В., Павлова Е.А. Использование Domain Specific Languages для моделирования программных систем. В сб. Современные технологии в задачах управления, автоматики и обработки информации: труды XVI Международного научно-технического семинара. - Тула: Изд-во ТулГУ, 2007. - 344 е., с. 43-44.

6. Павлова Е.А. Доменно-специфичный язык для разработки компьютерных игр в жанре пошаговых стратегий. В сб. НАУЧНАЯ СЕССИЯ МИФИ-2008. Сборник научных трудов. В 15 томах. Т.П. Технологии разработки программных систем. Информационные технологии. -М.: МИФИ, 2008.204 е., с. 58-59.

7. Павлова Е. А. Формальный предметно-ориентированный язык (DSL) для разработки компьютерных игр в классе пошаговых стратегий // Технологии Microsoft в теории и практике программирования: Труды V Всерос. конф. студентов, аспирантов и молодых ученых. Центральный регион. Москва, 1 - 2 апреля 2008 г. - М.: Вузовская книга, 2008.-е. 38-40.

8. Павлова Е. А. Формальный предметно-ориентированный язык (DSL) для описания правил компьютерных игр в классе пошаговых стратегий. Современные технологии в задачах управления, автоматики и обработки информации. Труды XVII международного научно-технического семинара. - СПб.: ГУАП, 2008, с. 260.

9. Pavlova Е. The Formal Approach to Computer Game Rule Development Automation // Proceedings of the Third Spring Young Researchers' Colloquium on Software Engineering (SYRCoSE 2009). Moscow, May 28-29,2009. - pp. 119-122.

10. Павлова E. А. Технологии разработки современных информационных систем на платформе Microsoft.NET: Учебное пособие / Е. А. Павлова - М.:Интернет-Университет Информационных технологий; БИНОМ. Лаборатория знаний, 2009. - 112 е.: ил., табл. - (Серия «Основы информационных технологий»).

И.Павлова Е. А. Разработка формального предметно-ориентированного языка описания правил игр // Технологии Microsoft в теории и практике программирования: Труды VI Всерос. конф. студентов, аспирантов и молодых ученых. Центральный регион. Москва, 1 - 2 апреля 2009 г. - М.: Вузовская книга, 2009. -с. 175-177.

12. Павлова Е.А. Об одном подходе к верификации компьютерных игр // НАУЧНАЯ СЕССИЯ НИЯУ МИФИ-2010. XIII Международная телекоммуникационная конференция студентов и молодых учёных «МОЛОДЁЖЬ И НАУКА». Тезисы докладов. В 3-х частях. 4.2. - Москва, НИЯУ МИФИ, 2010.- с.54-55.

13. Павлова Е. А. Метод разработки компьютерных игр класса пошаговых стратегий // Технологии Microsoft в теории и практике программирования: Труды VII Всерос. конф. студентов, аспирантов и молодых ученых. Центральный регион. Москва, 21-22 апреля 2010 г. - М.: Вузовская книга, 2010. -с. 123-124.

Отпечатано в ООО «Компания Спутник+» ПД № 1-00007 от 26.09.2000 г. Подписано в печать 25.05.2011 Тираж 100 экз. Усл. п.л. 1,0 Печать авторефератов (495)730-47-74,778-45-60

Введение.

1. Современное состояние проблемы разработки и верификации систем с пошаговыми стратегиями.

1.1. Обзор индустрии систем с пошаговыми стратегиями.

1.1.1. Особенности индустрии систем с пошаговыми стратегиями по сравнению с индустрией разработки программного обеспечения.

1.1.2. Особенности систем с пошаговыми стратегиями как программных систем.

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

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

1.2. Используемые подходы к разработке сложных информационных систем.

1.2.1. Понятие метода разработки программного обеспечения и структура метода.

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

1.2.3. Применение формальных языков в разработке логических компонентов систем с пошаговыми стратегиями.

1.2.4. Обзор методов проверки корректности правил систем с пошаговыми стратегиями.

1.3. Постановка задачи.

1.4. Выводы.

2. Модели и методы разработки логических компонентов систем с пошаговыми стратегиями.

2.1. Метод разработки логических компонентов систем с пошаговыми стратегиями.

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

2.1.2. Описание фрагментов процесса разработки.

2.1.3. Действующие лица.

2.1.4. Результаты разработки.

2.2. Теоретические основы предметно-ориентированного языка описания правил систем с пошаговыми стратегиями.

2.2.1. Синтаксис.

2.2.2. Семантика.

2.3. Верификация правил систем с пошаговыми стратегиями.

2.3.1. Проверка синтаксической и семантической совместности.

2.3.2. Верификация сбалансированности правил при помощи проверки на модели.

2.3.3. Сравнительная оценка сложности верификации модели правил при помощи проверки на модели и тестирования модели.

2.4. Выводы.

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

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

3.1.1. Основные требования к инструментальному средству.

3.1.2. Варианты использования инструментального средства.

3.1.3. Функции инструментального средства.

3.1.4. Требования к интерфейсу.

3.1.5. Концептуальная модель архитектуры инструментального средства.

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

3.2.1. Определение основных компонентов инструментального средства.

3.2.2. Описание динамики инструментального средства.

3.2.3. Основные классы, описывающие данные инструментального средства.

3.2.4. Основные классы интерфейса пользователя инструментального средства.

3.2.5. Основные классы транслятора модели правил и верификатора.

3.3. Физический уровень проектирования инструментального средства.

3.3.1. Физическое проектирование классов инструментального средства.

3.3.2. Проектирование компонентной архитектуры.

3.3.3. Разработка модели развёртывания инструментального средства.

3.4. Выводы.

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

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

4.1.1. Реализация предметно-ориентированного языка и компонентов для проектирования правил.

4.1.2. Особенности генератора прототипа систем с пошаговыми стратегиями.

4.1.3. Особенности реализации трансляции модели правил и верификации совместности.

4.1.4. Особенности реализации трансляции модели конфигурации и верификации сбалансированности.

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

4.3. Сравнение с предыдущими разработками.

4.4. Практическое приложение результатов.

4.5. Выводы.

Разработка систем с пошаговыми стратегиями является одним из самых динамично развивающихся направлений информационных технологий (ИТ) [1]. В 2008 году темпы роста этой области ИТ составили около 20% [2]. В работе [3] отмечается, что развитие аппаратного обеспечения современных компьютеров напрямую связано с состоянием дел в области разработки систем с пошаговыми стратегиями. В современных исследованиях, посвященных обучающим, в частности, развивающим информационным системам, существенное внимание уделяется технологиям их разработки на основе систем с пошаговыми стратегиями. Такие системы применяются в учебных заведениях [4-10], а также при подготовке специалистов на производстве и в военном деле [11-15]. Таким образом, разработка систем с пошаговыми стратегиями представляется актуальным и перспективным направлением ИТ.

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

Большинство исследователей [16-19] выделяют следующие компоненты, входящие в состав систем с пошаговыми стратегиями: графические, логические, физические, манипулирования данными, сетевые, звуковые, искусственного интеллекта. Логический компонент (logic engine) — компонент, инкапсулирующий правила и предоставляющий интерфейс, содержащий методы определения изменений состояния системы в результате действий пользователей.

В настоящей работе рассматриваются системы с пошаговыми стратегиями, в частности программы-тренажеры и игры. Термин "пошаговая" означает, что функционирование системы может быть описано с помощью упорядоченных во времени процессов, называемых ходами [20-22]. На обдумывание и выполнение хода даётся некоторое время. Смысл работы системы заключается в эффективном управлении некоторыми ресурсами, используя которые, необходимо добиться определенного результата, например, преимущества над противником. Обязательным является наличие оперативного плана, разрабатываемого с учётом меняющейся обстановки. Обычными ресурсами в военных стратегиях являются войска (отдельные персонажи, подразделения или армии) и позиция, которые следует развивать и использовать для достижения преимущества [20-25]. В экономических стратегиях акцент ставится на развитие экономической инфраструктуры, подконтрольной одной из сторон. Современные игры класса пошаговых стратегий, как правило, соединяют в себе как военные, так и экономические факторы. Согласно работе [4], игры класса пошаговых стратегий считаются одними из самых перспективных для использования в качестве основы для создания обучающих программ-тренажёров, так как развивают логическое и стратегическое мышление.

Системы с пошаговыми стратегиями имеют относительно простую архитектуру и предъявляют высокие требования только к функциональности логического компонента. Для создания системы с пошаговыми стратегиями необходимо разработать логический и графический компоненты, компонент искусственного интеллекта и компонент манипулирования данными. Основное внимание при разработке уделяется именно логическому компоненту [20-25], в качестве остальных компонентов при создании прототипа системы могут быть использованы готовые разработки сторонних специалистов. Понятная архитектура и возможность использования готовых компонентов позволяют проектировать системы с пошаговыми стратегиями в автоматизированном режиме.

Следует отметить, что индустрия систем с пошаговыми стратегиями, в частности, компьютерных игр характеризуется невысоким уровнем качества выпускаемой продукции по сравнению со средним уровнем качества в индустрии программного обеспечения в целом [26]. Одной из причин невысокого качества продуктов можно назвать несовершенство существующих методов и средств разработки. На текущем этапе развития индустрии не существует общепринятых методов и шаблонов разработки систем с пошаговыми стратегиями. Методы обычно создаются отдельными компаниями и зачастую меняются от проекта к проекту. Информация о методах обычно является закрытой [27], что затрудняет их повторное использование и модернизацию широким кругом разработчиков. Неформальные краткие описания подхода к созданию игр приводятся, например, в работах [16, 20, 23]. Однако основное внимание в описаниях уделяется проектированию архитектуры физического уровня, реализации отдельных компонентов игры и некоторым аспектам создания правил работы системы. Существуют работы [16, 22], затрагивающие вопрос логического проектирования, однако они в основном рассматривают применение шаблонов проектирования[28]. В литературе подробно рассмотрены методы разработки графических компонентов [20], компонентов, моделирующих физические процессы [17, 18, 20] и компонентов искусственного интеллекта [29—35]. Сравнительно мало исследований посвящено логическим компонентам игр, хотя именно они являются важнейшими составляющими систем с пошаговыми стратегиями.

Представление о применяемом в индустрии методе разработки логических компонентов можно составить, например, на основе работы Роллингса и Морриса [16]. В исследовательских работах явно отмечаются следующие виды деятельности, необходимые для создания логических компонентов: анализ предметной области, проектирование правил игры, реализация кода компонента на основе правил и тестирование. Как правило, проектирование правил и проверку результатов выполняет проектировщик правил функционирования систем с пошаговыми стратегиями[16, 18]. Он создаёт общую спецификацию, правила, описывает предполагаемый интерфейс системы и все возможные события, которые могут произойти с пользователем. Правила, являющиеся» основой логического компонента, обычно описываются неформально. Значительная часть правил представляется в виде обширных таблиц и слабо структурированных документов на естественном языке, которые могут содержать сотни страниц текста [16]. Процесс описания, модификации и проверки правил требует значительных ресурсов, в том числе временных и трудовых. Неформальное описание правил затрудняет применение формальных методов« для- проверки их корректности, автоматизацию процесса описания и проверки, а также повторное использование правил.

Традиционными языками разработчиков систем с пошаговыми стратегиями являются С и С++ [16, 36]; кроме того, часто используются ассемблерные вставки [16]. В связи с этим, реализация часто выполняется в среде разработки Microsoft Visual Studio. При реализации логического компонента и определении структур данных разработчики анализируют описания правил. Поскольку чаще всего используется неформальное описание правил, процесс реализации логического компонента требует значительных усилий и ресурсов. Естественно, затруднена и генерация кода на основе правил.

Проверка логических компонентов чаще всего выполняется путём тщательного просмотра кода и проектной документации и/или длительного тестирования кода без применения средств автоматизации. Часто отсутствует чёткое представление о проверяемых свойствах, так например, существует множество существенно отличающихся друг от друга представлений о свойстве сбалансированности [16-19]. Ряд свойств, например совместность, цикличность, непротиворечивость часто вообще не проверяется. Так как проверка осуществляется неформальными методами, по окончанию проверки не гарантируется выполнение конкретных свойств или их отсутствие. Проверка, в том числе правил функционирования системы на предмет сбалансированности, проводится главным образом после комплексной интеграции на этапе тестирования. Реально же нарушение свойств сбалансированности обычно происходит на этапе проектирования. Таким образом, выявление ошибок происходит на поздних этапах разработки, что повышает стоимость исправления ошибок и увеличивает время разработки.

Для создания более структурированных и лаконичных описаний,, позволяющих проектировщикам легче вносить изменения- в правила, приходится осваивать языки моделирования и программирования общего назначения и соответствующие инструменты (этот вопрос подробно рассматривается в работах [16, 17, 37-40]); что-требует значительных затрат времени и других ресурсов. В качестве альтернативы используются специализированные инструменты проектирования игр (информацию об этом можно найти в работах [17, 39; 4:1-43]), однако они не учитывают особенности систем с пошаговыми стратегиями, то есть не используется часть накопленного опыта, заведомо пригодная для повторного использования. Примерами могут служить типы сущностей, которые в рамках одного класса имеют устоявшийся набор основных свойств и методов, типы отношений между сущностями, условия выигрыша.- В указанных выше инструментах проектирования описание правил совмещается с описанием графической составляющей системы, а в ряде случаев с описанием элементов искусственного интеллекта. Такое совмещение затрудняет независимый анализ, проверку и модификацию компонентов игры, усложняет повторное использование, а также быструю разработку прототипа системы на основе правил. Указанные инструментальные средства не предполагают автоматизированную проверку игры. Повышение эффективности разработки и качества выпускаемых продуктов может быть достигнуто при помощи научных и технических методов, используемых в индустрии программного обеспечения.

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

Объектом исследования диссертационной работы являются системы с пошаговыми стратегиями.

Предмет исследования диссертационной работы — разработка логических компонентов систем с пошаговыми стратегиями.

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

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

• анализ существующих методов и инструментальных средств для проектирования, реализации и верификации логических компонентов систем с пошаговыми стратегиями;

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

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

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

• проектирование архитектуры системы поддержки разработки логических компонентов систем с пошаговыми стратегиями;

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

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

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

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

• новый формальный язык для описания правил систем с пошаговыми стратегиями;

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

• новый алгоритм статической проверки свойств совместности;

• новый алгоритм сокращения числа состояний для верификации свойств сбалансированности при помощи проверки на модели (model checking).

Практическая значимость результатов определяется следующим:

• реализован язык для описания правил систем с пошаговыми стратегиями. Язык учитывает особенности таких систем и позволяет проектировщику правил создавать графические описания правил в терминах предметной области;

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

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

Разработанное инструментальное средство для поддержки создания логических компонентов может применяться в процессе разработки совместно с другими средствами, используемыми при разработке систем с пошаговыми стратегиями (в том числе, средствами' для создания графических, физических или звуковых компонентов). Как правило, интеграция различных компонентов производится при помощи инструментальных средств семейства Microsoft Visual Studio (по данным работы [36], около 90% игр разрабатывается на языке С++ в среде Visual Studio). При этом часть существующих инструментальных средств интегрируется в Visual Studio, другие предоставляют программный интерфейс для интеграции или реализованы в виде программных библиотек, некоторые выдают в качестве выходных данных код на различных языках программирования, к которому можно обратиться из программных модулей, разрабатываемых в Visual Studio. Полученное в результате данной работы инструментальное средство интегрируется в Visual Studio, а в результате своей работы генерирует исходный код логического компонента на языке С#. За счет этого разработанное средство может быть использовано совместно с другими средствами разработки, а сгенерированные логические компоненты могут быть использованы без Visual Studio и интегрированы при помощи любого компилятора или интерпретатора языка С# в различные системы с пошаговыми стратегиями.

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

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

• на Научной сессии МИФИ в 2008 г.;

• на V Всероссийской конференции студентов, аспирантов и молодых ученых «Технологии Microsoft в теории и практике программирования» в 2008 г.;

• на Software Engineering Conference (Russia), SEC(R) в 2008 г.;

• на Научной сессии МИФИ в 2009 г.;

• на VI Всероссийской конференции студентов, аспирантов и молодых ученых «Технологии Microsoft в теории и практике программирования» в 2009 г.;

• на Third Spring Young Researchers' Colloquium on Software Engineering (SYRCoSE) в 2009 г.;

• на научном семинаре ИСП РАН в 2009 г.; • на Научной сессии МИФИ в 2010 г.

Основные положения, выносимые на защиту:

• результаты анализа методов проектирования, верификации и реализации логических компонентов систем с пошаговыми стратегиями;

• метод разработки логических компонентов систем с пошаговыми стратегиями, включающий: о модели процессов разработки логических компонентов систем с пошаговыми стратегиями; о формальный язык для описания правил систем с пошаговыми стратегиями; о формализованные свойства совместности и сбалансированности, которым должны удовлетворять правила систем с пошаговыми стратегиями; о алгоритм верификации совместности правил систем с пошаговыми стратегиями; о алгоритм сокращения числа состояний для верификации свойств сбалансированности при помощи проверки на модели (model checking);

• архитектура системы поддержки разработки логических компонентов систем с пошаговыми стратегиями;

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

4.5. Выводы

В настоящей главе рассмотрены особенности реализации инструментального средства поддержки разработки логических компонентов систем с пошаговыми стратегиями. Предметно-ориентированный язык, спроектированный в главе 2, был реализован при помощи инструментального средства DSL Tools для визуального создания предметно-ориентированных языков и инструментов. При реализации компонентов трансляции были использованы сторонние программные продукты Flex и Bison, а при реализации верификатора — инструментальные средства SPIN и Z3. В главе приведены данные о процессе тестирования инструмента. Было проведено модульное, интеграционное и системное тестирование, сделаны выводы о достижении инструментальным средством высокого уровня качества. В главе проведено сравнение разработанного инструментального средства с аналогичными системами, описаны внедрения инструментального средства и приведён пример его применения для описания и верификации правил. Сделан вывод о конкурентоспособности реализованного инструментального средства. В главе проведено испытание разработанного инструментального средства на примере программы-тренажёра ТасОрв, применяемого вооружёнными силами для подготовки военных специалистов. Была построена модель правил боевых действий для одной из кампаний, определённых в тренажёре. Была проведена верификация свойств сбалансированности моделей исходных и модифицированных правил, в результате которой был выявлен ряд нарушений свойств сбалансированности.

Заключение.

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

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

1. проведен анализ существующих методов разработки логических компонентов систем с пошаговыми стратегиями, представленных в публикациях. В частности, исследованы методы проектирования правил и методы обеспечения качества логических компонентов. На основе результатов анализа сделан вывод о недостаточности обеспечиваемого этими методами уровня качества логических компонентов и необходимости синтеза нового метода разработки;

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

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

4. для языка разработана- формальная спецификация, определяющая синтаксис и денотационную семантику языка. Спецификация позволяет применить формальные методы анализа к описаниям правил на этом языке;

5. формализованы свойства, которым должны удовлетворять правила. Разработан новый алгоритм верификации свойств совместности при помощи статического анализа и новый алгоритм сокращения числа состояний для верификации свойств сбалансированности при помощи проверки на модели (model checking). Предложенные алгоритмы позволяют автоматизировать проверку сформулированных свойств;

6. разработана архитектура системы поддержки разработки логических компонентов систем с пошаговыми стратегиями. Система поддерживает разработку логических компонентов при помощи предложенного метода создание на базе этого компонента исполнимого прототипа программы;

7. разработано программное обеспечение на основе архитектуры системы поддержки разработки логических компонентов. Разработанное программное обеспечение позволяет создавать системы с пошаговыми стратегиями при помощи предложенного метода разработки логических компонентов, используя предметно-ориентированный язык для, описания правил, и проводить верификацию при помощи предложенных алгоритмов. Разработанное программное обеспечение внедрено в практическую деятельность ОАО «Туристский информационный центр города Москвы» и деятельность компании ООО «Некки».

1. White W., Koch Ch., Gehrke J., Demers A. Better Scripts, Better Games // Communications of the ACM. No. 3. NY: ACM, 2009, pp. 42-47

2. ESA. Essential Facts About the Computer and Video Game Industry. -http://www.theesa.com/facts/pdfs/ESAEF2009.pdf, 2009

3. Piekarski W., Thomas B. ARQuake: the Outdoor Augmented reality gaming system // Communications of the ACM. V. 45,1. 1. NY: ACM, 2002. pp. 36-38

4. Hoffmann L. Learning through Games // Communications of the ACM. V. 52,1. 8. NY: ACM, 2009, pp. 21-22

5. Атанов Г.А. Компьютерные «игры» в обучение // Образовательные технологии и общество. №7. Выпуск 2. Казань: Казанский государственный технологический университет, 2004, с. 185-189

6. Сапунцов В.Д. Компьютерные деловые игры и дистанционное образование // Дистанционное образование. Дистанционное и виртуальное обучение, №1. -М.: СГУ, 2001, с. 14-20

7. Cannon-bowers J., Bowers С. Serious Game Design and Development: Technologies for Training and Learning. Information Science Publishing, 2010, 392 P.

8. Edvardsen Fr., Kulle H. Educational Games: Design, Learning and Applications (Education in a Competitive and Globalizing World). Nova Science Pub Inc, 2010

9. Meyer В., Sorensen В. H. Designing Serious Games for Computer Assisted Language Learning a Framework for Development and Analysis // Design and Use of Serious Games. - Springer Netherlands, 2010, pp. 69-83

10. Brox E., Heggelund A., Evertsen G. Comptence Complexity and Obvious Learning: Experience from Developing a Language Learning Game // Design and Use of Serious Games. Springer Netherlands, 2010, pp. 83-97

11. Iuppa N., Borst T. End-to-End Game Development: Creating Independent Serious Games and Simulations from Start to Finish. 1st Edition. Focal Press, 2009, 381 P.

12. Kankaanranta M., Neittaanmaki P. Design and Use of Serious Games. -Springer Netherlands, 2010, 216 P. '

13. Bergeron B. Developing Serious Games. Cengage Learning, 2006. 464 P.

14. Taylor M. J., Baskett M., Hughes G. D., Wade S. J. Using Soft Systems Methodology for Computer Game Design // Systems Research and Behavioral Science. #24. John Wiley & Sons, Ltd., 2007, pp.359-368

15. Chatham R., Braddock J., Training Superiority and Training Surprise // Report of the Defense Science Board. Washington: Office of The Under Secretary of Defence for Acquisition, Technology and Logistics, 2001, 41 P.

16. Rollings A., Morris D. Game Architecture and Design. A New EditionIndianapolis: New Riders Publishing, 2004

17. Wihlidal G. Game Engine Toolset Development.- Boston, MA: Thomson Course Technology PTR, 2006

18. Bates B. Game Design. Second Edition. Boston, MA: Thomson Course Technology PTR, 2004

19. Crawford Ch. The Art of Computer Game Design. NY: Mcgraw-Hill Osborne Media, 1984

20. Meigs T. Ultimate Game Design: Building Game Worlds. NY: McGraw-Hill/Osborne, 2003

21. Salen K., Zimmerman E. Rules of Play: Game Design Fundamentals. The MIT Press, 2003, 688 P.

22. Kreimeier B. The Case For Game Design Patterns // Gamasutra. N. 12. — http ://www.gamasutra.com/ vi ew/ feature/4261/ thecaseforgamedesignpatterns.php, 2002

23. Rabin St. Introduction to Game Development, 2nd Edition. Delmar Learning, 2010, 1016 P.

24. Rouse R. Ill Game Design: Theory and Practice (2nd Edition). — Jones & Bartlett Publishers, 2004, 584 P.

25. Wolf M. J. P., Baer R. H. The Medium of the Video Game. Austin, TX: University of Texas Press, 2002

26. Консалтинговая группа MD. http://www.md-consulting.ru/

27. Плюммер Дж. Гибкая и масштабируемая архитектура для компьютерных игр. http://www.dtf.ru/articles/read.php?id=40757, 2004

28. Gamma Е., Helm R., Johnson R., Vlissides J. Design Patterns. Elements of Reusable Object-Oriented Software. Massachusetts: Addison-Wesley Longman, Inc., 1995, 416 P.

29. Charles D., Fyfe C., Livingstone D., McGlinchey St. Biologically Inspired Artificial Intelligence for Computer Games. IGI Publishing, 2008, 279 P.

30. Millington I. Artificial Intelligence for Games. San Francisco: Elsevier, 2006, 895 P.

31. Корнилов E. Программирование шахмат и других логических игр. — СПб.: БХВ-Петербург, 2005, 272 с.

32. Leigh R., Schonfeld J., Louis S. J.Using Coevolution to Understand and Validate Game Balance in Continuous Games // Proceedings of the 10th annual conference on Genetic and evolutionary computation NY, USA : ACM New York, 2008, pp. 1563-1570

33. Andrade G., Ramalho G., Santana H., Corruble V. Automatic computer game balancing: a reinforcement learning approach // Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems. — NY: ACM, 2005, pp. 1111-1112

34. Kiefer P., Matyas S. The Geogames Tool: Balancing Spatio-Temporal Design Parameters in Location-Based Games // Proc. 7th International Conference on Computer Games (CGAMES 05). University of Wolverhampton, 2005, pp. 216-222

35. Dickheiser M. С++ For Game Programmers 2d edition. Charles River Media, 2006

36. Yang H-C. A General Framework for Automatically Creating Games for Learning // Proceedings of ICALT'05. IEEE, 2005, pp. 28-29

37. Meng L.S., Prakash E. C., Loh P. К. K. Design and Development of a Peer-to-Peer Online Multiplayer Game Using DirectX and C#. IEEE, 2004, pp. 278-281

38. McNaughton M., Cutumisu M., Szafron D., Schaeffer J:, Redford J., Parker D. Script-Ease: Generating Script-Code for. Computer Role-Playing Games // Proceedings of ASE'04. IEEE, 2004, pp.386-3 87

39. Chen W. Y., Payandeh S. Micro Robot Hockey Simulator'— Game Engine Design // Proceedings of CIG 2007. IEEE, 2007, pp. 9-16

40. Hu W. A Reusable Eduventure Game Framework // Transactions on Edutainment I. Berlin: Springer, 2008, pp. 74-85

41. Amory A. Game object model version II: a theoretical framework for educational game development // Educational Technology Research and Development. V.55, N. 1 / February, 2007. Boston: Springer, 2007, pp. 51 - 77

42. Бондарева T.B., Грызлова O.B., Евтюхин H.B. Компьютерные деловые игры как инновационное средство обучения // Телекоммуникации и информатизация образования, №1 (январь). М.: СГУ, 2001, с. 58-69

43. Lebram М., Backlund P., Engstrom Н., Johannesson М. Design and Architecture of Sidh a Cave Based Firefighter Training Game // Design and Use of Serious Games. - Springer Netherlands, 2010, pp. 19-33

44. Gonzalez N., Kalyakin I., Lyytinen H. RACER: A Non-Commercial Driving Game which Became a Serious Tool in the Research of Driver Fatigue // Design and Use of Serious Games. Springer Netherlands, 2010, pp. 171-186

45. Cockburn A. Writing Effective Use Cases. NJ: Addison-Wesley Professional, 2001

46. Виргерс К. Разработка требований к программному обеспечению. — М.: Издательско-торговый дом «Русская редакция», 2004

47. Buttazzo G., Lipari G., Abeni L., Caccamo M. Soft Real-Time Systems: Predictability vs. Efficiency (Series in Computer Science). Springer, 2005, 275 P.

48. Game Middleware. http://gamemiddleware.org, 2007

49. TorqueEngineAdvanced- ttp://www.garagegames.com/products/torque/tgea/ features/

50. FPS Creator. — http://www.darkgamestudio.com/

51. NeoAxisEngine. -http://www.neoaxisgroup.com/

52. Offset Engine http://www.projectoffset.com/game.html

53. Unreal Engine. http://www.unrealtechnology.com/

54. C4 Engine. http://www.terathon.com/c4engine/features.php

55. Moreno-Ger P., Martinez-Ortiz I., Sierra J. L., Fernandez-Manjon B. Language-Driven Development of Videogames: The <e-Game> Experience // Entertainment Computing ICEC 2006. - Berlin: Springer, 2006, pp. 153-164

56. Furtado A. W. В., Santos A. L. M., Ramalho G. L. A Computer Games Software Factory and Edutainment Platform'for Microsoft .NET // IET Software. Volume 1, Issue 6, December 2007. IEEE, 2007, pp.280 - 293

57. Bjorner D. What is a Method ? An Essay on Some Aspects of Software Engineering // Programming Methodology. V. 9. — New York: Springer-Verlag, 2003, pp. 175-203

58. ISO/IEC TR 19759:2005, Software Engineering Guide to the Software Engineering Body of Knowledge (SWEBOK), 210 P.

59. Wupper H., Meijer H. A Taxonomy for Computing Science. -http://www.cs.ru.nl/~wupper/taxonomy/R9713.doc, 1997

60. Weis D., Leukel Ji, Kirn S. A Method for Aligning Business Process Modeling and Software Requirements Engineering // Proceedings of the PRIMIUM Subconference CEUR Workshop Proceedings. V. 328. 2008. - http://ceur-ws.org/Vol-328/paper9.pdf

61. NASA. Formal Methods Specification And Analysis Guidebook For The Verification Of Software And Computer Systems, Volume II: A Practitioner's Companion. NASA-GB-001-97. http://eis.jpl.nasa.gov/quality/FormalMethods/document/ NASA gb2.pdf, 1997,245 P.

62. Karlsson F., Agerfalk P. J., Hjalmarsson- A. Method Configuration with Development Tracks and Generic Project Types // EMMSAD'Ol. -http://www.om.se/org/instyesa/personal/pak/Karlssonetal2001EMMSAD.pdf

63. Motoshi Saeki and Haruhiko KaiyaModel Metrics and Metrics of Model Transformation // Workshop Materials of the 1 Workshop on Quality in Modeling. — Technische Universiteit Eindhoven, 2006, pp. 31-47

64. Sunyaev A., Hansen M., Krcmar H. Method Engineering: A Formal Description // Information Systems Development. Springer US, 2009, pp. 645-655 •

65. ISO/IEC 24744:2007 Software Engineering Metamodel for Development Methodologies. - IEEE, 2007, 87 P.

66. Greenfield J., Short K. Software Factories: Assembling Applications with Patterns, Models, Frameworks, and Tools. — Wiley, 2004

67. Kleppe A. MDA Explained, The Model Driven Architecture: Practice and Promise. Addison-Wesley, 2003, 192 P.

68. Cook St., Jones G., Kent S., Wills A. C. Domain-Specific Development with Visual Studio DSL Tools. Addison-Wesley Professional, 2007, 576 P.72. 12th International Software Product Line Conference (Splc 2008). IEEE Computer Society Press, 2009, 397 P.

69. HeroEngine. Программное средство для разработки MMOG, 2010. — http://www.heroengine.com/objects.asp

70. Yang H.-C. A General Framework for Automatically Creating Games for Learning // Proceedings ICALT'05. IEEE, 2005, pp. 28-29

71. Tsushima К. Progress toward the Science of game and amusement // Proceedings of the 2005 International Conference on Active Media Technology (AMT 2005). IEEE, 2005, pp. 259-262

72. Bruce K. Foundations of Object-Oriented Languages: Types and Semantics. — Cambridge, Massachusetts: The MIT Press, 2002

73. Кларк, Э. M., Грамберг О. Мл., Пелед Д. Верификация моделей программ: Model Checking. М: Издательство Московского центра непрерывного математического образования, 2002

74. Кулямин В.В. Методы верификации программного обеспечения // Всероссийский конкурсный отбор обзорно-аналитических статей по приоритетному направлению "Информационно-телекоммуникационные системы", 2008, 117 с.

75. Карпов Ю.Г. Model Checking. Верификация параллельных и распределённых программных систем. — СПб.: БХВ-Петербург, 2010, 560 с.

76. Fisher К., Mitchel J. С. The Development of Type Systems for Object-Oriented Languages // Theory and Practice of Object Systems. V.l. I. 3. — New York: John Wiley & Sons, Inc., 1995, pp. 189-220

77. Bruce К. В., Cardelli L., Pierce В. C. Comparing Object Encodings // Theoretical Aspects Of Computer Software. Lecture Notes in Computer Science. V.1281/1997. Springer, 1997, pp. 415-438

78. Abadi M., Cardelli L. A Theoiy of Objects. New York: Springer, 1996

79. Мейер Б. Объектно-ориентированное конструирование программных систем. — М.: Русская Редакция, 2005

80. Slonneger К., Kurtz В. L. Formal Syntax and Semantics of Programming Languages. A Laboratory Based Approach. N.Y.: Addison Wesley, 1995

81. Mosses P. D. Fundamental Concepts and Formal Semantics of Programming Languages — An Introductory Course. — http://wiki.daimi.au.dk/dSprogSem-01, 2002

82. Hoare C. An Axiomatic Basis of Computer Programming. Communications of the ACM. V. 12. New York: ACM Press, 1969

83. Гаврилов А.В., Павлова' Е. А. Формализация проектирования сложных информационных систем на основе анализа функциональных интерфейсов // Информационные технологии №9, 2008. М.: Новые технологии, 2008, с. 9-15

84. Chiu К. S.Y., Chan К. С.С. Using Data Mining for Dynamic Level Design in Games // ISMIS 2008, LNAI 4994. Springer-Verlag Berlin Heidelberg, 2008, pp. 628637

85. Hurwicz L., Reiter St. Designing Economic Mechanisms. — Cambridge University press, 2006, 344 P.

86. Birge J. R., Louveaux F. Introduction to Stochastic Programming. Springer, 1997, 448 P.

87. ACL 2. Инструментальное средство автоматического доказательства теорем. http://www.cs.utexas.edu/users/moore/acl2/

88. Е. Инструментальное средство автоматического доказательства теорем. http://www4.informatik.tu-muenchen.de/~schulz/W ORK/eprover.html

89. KeY. Инструментальное средство автоматического доказательства теорем. http://www.key-project.org/

90. Holzmann G. J. The Model Checker SPIN // IEEE Transaction on Software Engineering. 1997. Vol. 23. No.5. IEEE, 1997, pp. 279-295

91. NuSMV. http://nusmv.irst.itc.it/

92. Bogor. Инструментальное средство верификации при помощи проверки на модели. — http://bogor.projects.cis.ksu.edu

93. UPPAAL. Инструментальное средство верификации при помощи проверки на модели, —http://www.uppaal.com/

94. KRON0S. Инструментальное средство верификации; при. помощи проверки на модели. http://www-verimag.imag.fr/temporise/kronos/

95. CPN Tools. Инструментальное- средство верификации. при помощи проверки на модели. — http://daimi.au.dk/CPNTools/

96. Ахо А. В., Сети P., Ульман Д.Д. Компиляторы: принципы, технологии и инструменты.-М.: Издательский дом,"Вильяме", 2003

97. Schmidt D. A. Denotational Semantics. A methodology for Language Development. — William С Brown Pub, 1997

98. Филд А., Харрисон И. Функциональное программирование: M.: Мир,1993

99. Finkel R. A. Advanced Programming Language Design. — Menlo Park, CA: Addisson-Wesley, 1996

100. Павлова E.A. Проектирование формального предметно-ориентированного языка (DSL) для разработки правил компьютерных игр в классе пошаговых стратегий//Вестник компьютерных и информационных технологий №4, 2009 М.: Машиностроение, 2009, с. 45-52

101. Gavrilov A., Pavlova Е. DSL Tools for Model-Driven Development. Proceedings of the Software Engineering Conference (Russia), SEC(R) 2006, Moscow, RusSE-TEKAMA. http://secr.ru/2006/upload/files/107.pdf, 2006

102. Ефимова Е.Г., Заславская М.Д., Потапова И.С., Резякова H.A. Экономическая теория. Ч. 2 Макроэкономика. Издательство МГИУ, 2008, 243с.

103. Andrade G., Ramalho G., Gomes A. S. , Corruble V. Dynamic Game Balancing: an Evaluation of User Satisfaction // Proceedings of the 4rd Brazilian

104. Workshop on Computer Games and:Digital! Entertainment (WJogosOS). AAAI Press, 2005, pp. 66-76.

105. Fernandez M. Models of Computation: An Introduction to Gomputability Theory (Undergraduate Topics in Computer Science). Springer, 2009, 184 P.'

106. Разборов A.A. О сложности, вычислений // Математическое просвещение. Вып.З.- М.: МЦНМО, 1999¡ с. 127-141120: SPIN. http://spinroot.com

107. М. Вгоу, В. Jonsson, J.-P. Katoen, М. Leucker, A. Pretschner (eds.). Model Based Testing of Reactive Systems // LNCS 3472. Springer, 2005, 659 P.

108. Павлова E.A. Станкевичус A.A. Исследование сложности верификации моделей для правил логических компонентов с учётом свойств безопасности // Безопасность информационных технологий. №4. — М., 2009, с. 126-129

109. Анализ требований и создание архитектуры решений; на основе Microsoft.NET. Учебный курс MCSD. М.: Издательско-торговый, дом «Русская редакция», 2004

110. Microsoft Visual Studio 2008. http://msdn.microsoft.com/en-us/vstudio/default.aspx

111. Буч Г., Рамбо Д., Джекобсон А. Язык UML. Руководство пользователя. -М.: ДМК Пресс, 2001

112. Просиз Дж. Программирование для Microsoft.NET. — М.: Издательско-торговый дом «Русская редакция», 2003

113. Платт Д.С. Платформа Microsoft 2005. — М.: Издательско-торговый дом «Русская редакция», 2004

114. Павлова Е. А. Технологии разработки современных информационных систем на платформе Microsoft.NET: Учебное пособие / Е. А., Павлова\

115. М.:Интернет-Университет Информационных технологий; БИНОМ. Лаборатория знаний, 2009, 112 с.

116. Рихтер Дж. Программирование на платформе Microsoft .NET Framework.- М.: Издательско-торговый дом «Русская редакция», 2002'

117. Z3. http://research.microsoft.com/en-us/um/redmond/projects/z3/

118. Bjorner N., de Moura L. Z3A10 : Applications, Enablers, Challenges and Directions // Proceedings of CFV 2009. — 2009. http://research.microsoft.com/en-us/um/people/leonardo/cfV09:pdf

119. Котляров В.П. Основы тестирования программного обеспечения. — М.: Интернет-университет информационных технологий — ИНТУИТ.ру, 2006

120. Брауде Э. Технология разработки программного обеспечения. СПб.: Питер, 2004

121. Сергиевский М.В., Фотин Д.В. и др. Программное обеспечение центра управления информационными киосками // Вестник компьютерных и информационных технологий №3, 2010. -М.: Машиностроение, 2010, с. 50-56^

122. TacOps 4 Overview. - http://www.battlefront.com/index.php?option= comcontent&task=blogcategory&id=l 15&Itemid=165, 2008

123. Abbass H. A., Essam D. Applications of information systems to homeland security and defense. Idea Group Publishing, 2005, 257 P.

124. English J. The Instrumentality Of Armed Force And The Role Of The Canadian Army // Journal of Military and Strategic Studies. V. 6, I. 3. — Calgary: University of Calgary, 2004, pp. 1-14

125. Carpenter R., White.CI. Computer Games in The Australian Department Of Defence // Proceedings of SimTecT 2005. www.siaa.asn.au/get/2411856219.pdf, 2005

126. McFarlane D., Kruzins E. Australian Defence Simulation — Status. Canberra: Australian Defence Simulation Office, 2006, 46 P.

127. Clemons W. R. The Case for Consolidating Tactical and Operational Systems // The Land Warfare Papers. N. 52. Arlington: The Institue of Land Warfare, 2005, pp.l-21

128. James D. R., Dyer J. L., Wampler R. L. Exploring the Potential Value of OneSAF at the Small-Unit Level. U.S. Army Research Institute for the Behavioral and Social Sciences, 2008, 110 P.

129. TacOps Version 4 User Guide. http://www.battlefront.com/index.php7option =comflippingbook&bookid=3&Itemid=224, 2008