Model Checking in Multiplayer Games Development
Model Checking in Multiplayer Games Development
复制标题
多人游戏开发中的模型检查
DOI：
10.1109/aina.2018.00122
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
V. Rivera
中科院分区：
文献类型：
--
作者：
R. Rezin;Ilya M. Afanasyev;M. Mazzara;V. Rivera
多人电脑游戏在不断发展的娱乐产业中发挥着重要作用。在这个行业中保持竞争力意味着发布最好的软件，而可靠性是赢得市场的关键特征。计算机游戏也被积极用于模拟不同的机器人系统，其中可靠性更为重要，并且可能至关重要。传统的软件测试方法只能检查所有可能的程序执行的子集，并且永远不能保证源代码中完全不存在错误。另一方面，二十多年来，模型检查已被证明是大型硬件和软件组件形式验证的强大工具。在本文中，我们提出了一种新颖的方法来正式验证计算机游戏。我们提出了一种从计算机游戏描述开始并利用模型检查技术的模型构建方法。我们将该方法应用于案例研究：游戏《Penguin Clash》。最后，介绍了一种游戏模型简化方法（及其实现），以解决状态爆炸问题。
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.
DOI：
10.1007/s10009-015-0378-x
发表时间：
2017-02-01
影响因子：
1.5
作者：
Lomuscio, Alessio;Qu, Hongyang;Raimondi, Franco
通讯作者：
Raimondi, Franco