ИССЛЕДОВАНИЕ СЛОЖНОСТИ ВЕРИФИКАЦИИ МОДЕЛЕЙ ДЛЯ ПРАВИЛ ЛОГИЧЕСКИХ КОМПОНЕНТОВ С УЧЕТОМ СВОЙСТВ БЕЗОПАСНОСТИ

Е. А. Павлова, А. А. Станкевичус

Аннотация


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

Полный текст:

PDF

Литература


1 Androvich M. Forbes: Europe is least mature videogame market, 2008. http://www.gamesindustry.biz/articles/forbes-europe-is-least-mature-videogame-market.

2 Bono S., Caselden D., Landau G., Miller C. Reducing the Attack Surface in Massively Multiplayer Online Role-Playing Games // IEEE Security and Privacy. 2009. Vol. 7. № 3. P. 13-19.

3 Rollings A., Morris D. Game Architecture and Design. A New Edition. New Riders Publishing. Indianapolis, 2004. - 960 р.

4 Pavlova E. 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. - P. 119-122.

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

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

7 Holzmann G. J. The Model Checker SPIN // IEEE Transaction on Software Engineering. 1997. Vol. 23. № 5. P. 279-295.

8 Broy M., Jonsson B., Katoen J.-P., Leucker M., Pretschner A. (eds.). Model Based Testing of Reactive Systems. LNCS 3472. Springer, 2005. - 659 р.


Ссылки

  • На текущий момент ссылки отсутствуют.


Лицензия Creative Commons
Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.