Hunting for Bugs in Source Code of Video and Computer Games

寻找视频和电脑游戏源代码中的错误

• 批准号: RGPIN-2014-04406
• 负责人: vanBreugel, Franck
• 金额: $ 2.33万
• 依托单位: York University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2015
• 资助国家: 加拿大
• 起止时间: 2015-01-01 至 2016-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=587789
• 关键词: Hunting; Bugs; Source; Code; Video

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.

我们研究的目的是开发工具来检测视频和计算机游戏中的错误。而不是将众所周知的技术应用到游戏中，我们专注于在游戏中寻找bug时遇到的基本问题。我们预期的解决方案不仅会影响游戏行业，还会影响其他应用领域和学术界。 测试是检测bug最常用的方法。它对于确定性代码特别有效，即，对于固定的输入，只执行一次的代码。然而，在非决定论的存在下，即，当存在不同的潜在执行时，测试是不太有效的。多次运行测试并不能保证已经检查了不同的执行。此外，如果发现了bug，可能很难复制。因此，为了检测不确定性代码中的错误，需要补充测试的方法。 模型检查是测试的一种替代方法。与测试中所做的检查单个执行不同，模型检查试图系统地检查所有潜在的执行。然而，潜在执行的数量可能是代码中不确定性选择数量的指数。处理如此大量的执行的基本问题被称为状态空间爆炸问题。 随机性和并发性是当今游戏的关键要素，两者都导致了非决定论。因此，模型检查似乎是一个可行的替代测试发现游戏中的错误。虽然已经开发了许多模型检查器，但我们不知道任何可以验证游戏源代码属性的模型检查器。我们的总体目标是开发第一个这样的模型检查器。我们的主要目标是打击臭名昭著的状态空间爆炸所造成的随机和并发的组合。 我们专注于直接与源代码一起工作的模型检查器。我们首先将注意力限制在Java上，它是目前最流行的编程语言。虽然C++在游戏中使用最广泛，但许多游戏，特别是在线游戏，都是用Java编写的。例如，根据吉尼斯世界纪录，用Java实现的RuneScape是世界上最受欢迎的免费大型多人在线角色扮演游戏，拥有超过2亿注册帐户。 游戏的Java代码包含本机调用，即，这些调用调用了用不同于Java的语言编写的代码。例如，与图形、网络和声音相关的调用通常是本机的。使用本机调用对Java代码进行模型检查通常涉及在Java中对本机代码进行建模，这既耗时又容易出错。为了使我们的工具能被游戏开发者使用，本机调用应该被自动处理。这是我们的第二个主要目标。 玩家通过视频游戏控制器、鼠标、键盘等与游戏进行交互。为了对游戏进行模型检查，我们需要合并玩家的模型。理想情况下，模型应该从游戏的源代码中自动构建，这样我们的工具就容易被游戏开发人员使用。我们的第三个目标是尽可能自动生成玩家的模型。 加拿大的视频和电脑游戏产业是世界上最大的产业之一。它每年为加拿大经济贡献近20亿美元。由于我们的工具将允许游戏开发人员自动发现错误，它们将提高游戏的质量并提高游戏开发人员的生产力。 我们希望我们的研究结果也能影响其他应用领域和学术界。例如，在Java工具包中实现的通信协议中查找错误的工具，其中包含大量的本机调用，应该从我们处理本机调用的技术中受益。