Executable Formal Specifications in Game Development: Design, Validation and Evolution

Abstract

Suoritettavat formaalit spesifikaatiot pelikehityksessä: suunnittelu, validointi ja evoluutio

Digitaalisten pelien merkitys on nykyään valtava sekä viihteenä että taloudellisesti. Pelit voivat olla hyvin monimutkaisia, joka tekee pelin kehityksestä ja suunnittelusta haastavaa. Monimutkaisuus ilmenee varsinkin peleissä, jotka tukevat samanaikaisesti useita pelaajia ja peleissä, jotka voivat muuttua vielä julkaisun jälkeen.

Tässä tutkimuksessa ratkaistaan monimutkaisuuden hallintaa formaalien spesifikaatioiden avulla. Formaaleja spesifikaatioita voidaan käyttää pelien käyttäytymisen mallintamiseen tiiviisti korkealla tasolla. Toiminnallisuuden spesifiointi voidaan näin suorittaa huomattavasti nopeammin kuin mitä itse pelin toteuttamiseen menisi.

Tutkimuksessa esitetyt ratkaisut mahdollistavat mahdollisten pelitilanteiden simuloimisen todennäköisyyksien avulla koko pelikehitysprosessin aikana varhaisesta suunnitteluvaiheesta pelin julkaisun jälkeisiin muutoksiin.

Formaaleja menetelmiä hyödyntävän pelikehitysprosessin tarkoitus on tuottaa parempilaatuisia pelejä ja vähentää ongelmia pelin kehityksen aikana.

Games provide players with enjoyment, escapism, unique experiences and even a way to socialise. Software based games played on electronic devices such as computers and games consoles are a huge business that is still growing. New games are continually developed as demand for these digital games is high. Digital games are often complex and have high requirements for quality. The complexity is especially apparent in complex multiplayer games and games that are constantly evolving. This complexity can be problematic in various stages of development. For example, understanding if a design of a game works as intended can be difficult. Managing changes that need to be made to a game during its lifetime, even after its initial release, is also challenging from both a design and an implementation standpoint. In this thesis these problems are addressed by presenting a method of utilising formal methods for simulations of game designs as a way of development, communication, documentation and design. Formal methods are methods that aim to help developers create better software through the usage of tools and notations based on formal syntax and semantics. A specific sub-area of formal methods, namely executable formal specifications, was chosen as a starting point. This is because the executability of the specification makes it possible to simulate game progression which can be used to understand and communicate the design of a game better. The DisCo methodology and language are an implementation of executable formal specifications and feature an action based execution model. This toolset and language was modified and extended to make it more suitable to game development based on findings made in a series of case studies. In the case studies, specifications are created based on two existing games and one new design. The case studies also lead to discoveries in what features a methodology and tool for formal specifications in a game development process requires. Formal methods can be applied fairly naturally in game design. Because games are defined with rules, and due to the complexity of many games, methods are needed to manage that complexity. Action-based, executable methods fit especially well. Game development can benefit from formal methods if the methodology and tools are easy to use and the methodology incorporates properties, such as probabilities, deemed to be important for game specifications. The benefits apply to the whole development cycle of a game. A development process which includes formal methods can result in less problems during development and games of better quality.