litceysel.ru
добавить свой файл
1

УДК 004.4(06) Технологии разработки программных систем


Е.А. ПАВЛОВА

Научный руководитель – М.В. СЕРГИЕВСКИЙ, к.т.н., доцент

Национальный исследовательский ядерный университет «МИФИ»


ОБ ОДНОМ ПОДХОДЕ К ВЕРИФИКАЦИИ
КОМПЬЮТЕРНЫХ ИГР



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


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

В настоящей работе были формализованы свойства, проверка которых наиболее часто рассматривается в литературе. Свойства подразделяются на свойства совместности и сбалансированности. Совместность рассматривается применительно к компонентной модели игры и объектной модели компонента правил игры. Для верификации этого свойства взаимодействующие компоненты игры формально описываются при помощи расширения λς-исчисления [3] и проверяется корректность контрактов между интерфейсами компонент по методу, описанному в работе [4]. Объектная модель компонента правил игры представляется на разработанном ранее языке[5], для которого определена денотационная семантика, использующая объекты λς-исчисления. Совместность объектной модели правил проверяется аналогично совместности компонентной модели игры.


Сбалансированность правил представляет собой группу свойств, специфичных для предметной области компьютерных игр. Свойства широко трактуются в литературе [1,2]. Все свойства касаются сравнения состояний игроков в определённые моменты игры. Наиболее часто рассматриваемые свойства были формализованы в виде выражений логики линейного времени LTL[6]. Кроме того, было формализовано понятие «состояние игрока» и предложен способ его расчёта для игр класса пошаговых стратегий. Полученные таким образом формальные свойства верифицируются методами проверки на модели (model checking)[6].

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

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

На основе предложенного подхода к верификации игр был разработан прототип инструментального средства поддержки верификации игр в классе пошаговых стратегий. Инструмент использует компоненты системы для проверки выполнимости логических формул первого порядка и инструментальное средство SPIN[6] для верификации при помощи моделей.


Список литературы


1. Rollings A., Morris D. Game Architecture and Design. A New Edition.– Indianapolis: New Riders Publishing, 2004

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

3. Abadi M., Cardelli L. A Theory of Objects. – New York: Springer, 1996


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

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

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