基于符号模型检测对节点式可视化脚本进行形式化验证
软件工程
2022-01-04 v2
摘要
具有节点式界面的可视化脚本语言已普遍用于电子游戏行业。我们检查了《最终幻想 XV》（FFXV）开发中获取的缺陷数据库，注意到几类缺陷由可视化脚本的简单错误描述引起，因此可被机械检测。我们提出一种可视化脚本自动验证方法，以提高电子游戏开发的生产率。我们的方法可通过使用符号模型检测自动检测这些缺陷。我们展示了一种翻译算法，可自动将可视化脚本转换为符号模型检测实现 NuSMV 的输入模型。作为初步评估，我们将该方法应用于 FFXV 制作中使用的可视化脚本。评估结果表明，我们的方法能够检测脚本缺陷，并在合理时间内良好工作。
引用
@article{arxiv.2103.11618,
title = {Formal Verification for Node-Based Visual Scripts Using Symbolic Model Checking},
author = {Isamu Hasegawa and Tomoyuki Yokogawa},
journal= {arXiv preprint arXiv:2103.11618},
year = {2022}
}