Hunting for Bugs in Source Code of Video and Computer Games

点击翻译按钮获取中文摘要

The aim of our research is to develop tools to detect bugs in video and computer games. Rather than applying well-known techniques to games, we focus on fundamental problems that are encountered when hunting for bugs in games. Our anticipated solutions will not only impact the game industry but also other application areas and academia. Testing is the most commonly used method to detect bugs. It is particularly effective for deterministic code, i.e., code that for a fixed input gives rise to a single execution. However, in the presence of nondeterminism, i.e., when there are different potential executions, testing is less effective. Running a test multiple times provides no guarantee that different executions have been checked. Also, if a bug has been found, it may be difficult to reproduce. Therefore, to detect bugs in nondeterministic code, methods that complement testing are needed. Model checking is an alternative to testing. Rather than checking a single execution, as is done in testing, model checking attempts to systematically check all potential executions. However, the number of potential executions can be exponential in the number of nondeterministic choices in the code. The fundamental problem of dealing with such a huge number of executions is known as the state space explosion problem. Randomization and concurrency, which are key ingredients of today’s games, both give rise to nondeterminism. Therefore, model checking seems a viable alternative to testing for finding bugs in games. Although numerous model checkers have been developed, we are not aware of any that can verify properties of the source code of games. Our overall aim is to develop the first such model checker. Our main objective is to combat the notorious state space explosion caused by a combination of randomization and concurrency. We focus on model checkers that work directly with the source code. We initially restrict our attention to Java, currently the most popular programming language. Although C++ is most widely used for games, many, in particular online games, are written in Java. For example, according to Guinness World Records, RuneScape, implemented in Java, is the world's most popular free massively multiplayer online role-playing game with more than 200 million registered accounts. The Java code of games contains native calls, i.e., calls which invoke code that is written in a language different from Java. For example, calls related to graphics, networking and sound are usually native. Model checking Java code with native calls usually involves modelling the native code in Java, which is time consuming and error-prone. To make our tools of use to game developers, native calls should be handled automatically. This is our second major objective. Players interact with a game by means of the video game controller, the mouse, the keyboard, etc. In order to model check a game, we need to incorporate a model of the players. Ideally, the models should be built automatically from the source code of the game, so that our tools are easy to use by game developers. Our third objective is to automate the generation of models of the players as much as possible. The Canadian video and computer game industry is among the largest in the world. It contributes almost two billion dollars per year to the Canadian economy. Since our tools will allow game developers to find bugs automatically, they will improve the quality of the games and increase the productivity of game developers. We expect our results to also impact other application areas and academia. For example, tools to find bugs in communication protocols implemented in Java toolkits, which contain numerous native calls, should benefit from our techniques to handle native calls.