Model Checking in multiplayer games development
This addresses reliability issues for game developers and robotic system designers, though it appears incremental as it adapts existing Model Checking techniques to a new domain.
The paper tackles the problem of ensuring reliability in multiplayer computer games and robotic simulations by proposing a novel method for formal verification using Model Checking, applied to the game Penguin Clash and including a model reduction approach to handle state explosion.
Multiplayer computer games play a big role in the ever-growing entertainment industry. Being competitive in this industry means releasing the best possible software, and reliability is a key feature to win the market. Computer games are also actively used to simulate different robotic systems where reliability is even more important, and potentially critical. Traditional software testing approaches can check a subset of all the possible program executions, and they can never guarantee complete absence of errors in the source code. On the other hand, during more than twenty years, Model Checking has demonstrated to be a powerful instrument for formal verification of large hardware and software components. In this paper, we contribute with a novel approach to formally verify computer games. We propose a method of model construction that starts from a computer game description and utilizes Model Checking technique. We apply the method on a case study: the game Penguin Clash. Finally, an approach to game model reduction (and its implementation) is introduced in order to address the state explosion problem.