Abstract
Visual script languages with a node-based interface have commonly been used in the video game industry. We examined the bug database obtained in the development of FINAL FANTASY XV (FFXV), and noticed that several types of bugs were caused by simple mis-descriptions of visual scripts and could therefore be mechanically detected.
We propose a method for the automatic verification of visual scripts in order to improve productivity of video game development. Our method can automatically detect those bugs by using symbolic model checking. We show a translation algorithm which can automatically convert a visual script to an input model for NuSMV that is an implementation of symbolic model checking.
For a preliminary evaluation, we applied our method to visual scripts used in the production for FFXV. The evaluation results demonstrate that our method can detect bugs of scripts and works well in a reasonable time.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
“fade out” is a gradual transition from the game screen to blank image, used in movies, games, etc.
- 2.
There are a few exceptions such as a node that can accept 2 inputs simultaneously, we address them in Sect. 4.2.
- 3.
According to the game designers, those scripts are used only in the trial version, so they will not fix the bugs though.
References
Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica 20(3), 207–226 (1983)
Berezin, S., Campos, S., Clarke, E.M.: Compositional reasoning in model checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 81–102. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49213-5_4
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hawng, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)
Chan, W., et al.: Model checking large software specifications. IEEE Trans. Softw. Eng. 24(7), 498–520 (1998)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48683-6_44
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
FINAL FANTASY XV. http://www.jp.square-enix.com/ff15/
Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)
Hasegawa, I., Nozoe, R., Ono, T., Koyama, M., Ishida, T.: Visual effects of final fantasy XV: concept, environment and implementation. In: ACM SIGGRAPH 2016 Talks, SIGGRAPH 2016, pp. 23:1–23:2. ACM, New York (2016)
Jussila, T., et al.: Model checking dynamic and hierarchical UML state machines. In: Proceedings of the 3rd International Workshop on Model Development, Validation and Verification (MoDeVa 2006), pp. 94–110 (2006)
Leveson, N.G., Heimdahl, M.P.E., Hildreth, H., Reese, J.D.: Requirements specification for process-control systems. IEEE Trans. Softw. Eng. 20(9), 684–707 (1994)
Lumberyard Script Canvas. https://docs.aws.amazon.com/lumberyard/latest/userguide/script-canvas-intro.html
Moreno-Ger, P., Fuentes-Fernández, R., Sierra-Rodríguez, J.L., Fernández-Manjón, B.: Model-checking for adventure videogames. Inf. Softw. Technol. 51(3), 564–580 (2009)
Pnueli, A.: A temporal logic of concurrent programs. Theor. Comput. Sci. 13, 45–60 (1981)
Radomski, S., Neubacher, T.: Formal verification of selected game-logic specifications. In: Proceedings of the 2nd EICS Workshop on Engineering Interactive Computer Systems with SCXML, pp. 30–34 (2015)
Rezin, R., Afanasyev, I., Mazzara, M., Rivera, V.: Model checking in multiplayer games development. In: 2018 IEEE 32nd International Conference on Advanced Information Networking and Applications (AINA), pp. 826–833 (2018)
Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual, 2nd edn. Pearson Higher Education, London (2004)
Unreal Engine 4 Blueprints. https://docs.unrealengine.com/en-US/Engine/Blueprints/
Zhao, Q., Krogh, B.H.: Formal verification of statecharts using finite-state model checkers. IEEE Trans. Control. Syst. Technol. 14(5), 943–950 (2006)
Acknowledgment
We wish to thank the collaborative researchers for helpful discussions. We also wish to thank the FINAL FANTASY XV development team for supporting our research. UNREAL ENGINE is a trademark or registered trademark of Epic Games, Inc. Windows is a trademark or registered trademark of Microsoft Corporation. All other trademarks are the property of their respective owners.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Hasegawa, I., Yokogawa, T. (2019). Automatic Verification for Node-Based Visual Script Notation Using Model Checking. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-32409-4_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32408-7
Online ISBN: 978-3-030-32409-4
eBook Packages: Computer ScienceComputer Science (R0)