Hunting for Bugs in Source Code of Video and Computer Games

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

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

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