Modeling and verification of chess game using NuSMV

Vikram Saralaya, J. K. Kishore, Sateesh Reddy, Radhika M. Pai, Sanjay Singh

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Gaming industry has always relied on testing their product by playing it extensively. However, testers have their own limitations. When such a product is deployed, extreme gamers find those bugs that were overlooked by the testers. Hence testing is a best-effort service and does not assure that a particular product is working bug free. Application of formal methods to games is a vast area, but less explored. It has been applied to some of the simple games like Tic-Tac-Toe, Rush-Hour etc. Formalizing a chess game is complex since the game can enter a countably infinite number of states. In this paper we build a model which takes a sequence of moves (called as "Notation" in Chess Community) as input and verify that standard rules of the game are not violated. Specifications are written using LTL (Linear-Time Temporal Logic). We have used NuSMV (extension of Symbolic Model Verifier) as a model checking tool to verify the LTL specifications.

Original languageEnglish
Title of host publicationAdvances in Computing and Communications - First International Conference, ACC 2011, Proceedings
Pages460-470
Number of pages11
Volume191 CCIS
EditionPART 2
DOIs
Publication statusPublished - 2011
Event1st International Conference on Advances in Computing and Communications, ACC 2011 - Kochi, India
Duration: 22-07-201124-07-2011

Publication series

NameCommunications in Computer and Information Science
NumberPART 2
Volume191 CCIS
ISSN (Print)1865-0929

Conference

Conference1st International Conference on Advances in Computing and Communications, ACC 2011
CountryIndia
CityKochi
Period22-07-1124-07-11

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Cite this

Saralaya, V., Kishore, J. K., Reddy, S., Pai, R. M., & Singh, S. (2011). Modeling and verification of chess game using NuSMV. In Advances in Computing and Communications - First International Conference, ACC 2011, Proceedings (PART 2 ed., Vol. 191 CCIS, pp. 460-470). (Communications in Computer and Information Science; Vol. 191 CCIS, No. PART 2). https://doi.org/10.1007/978-3-642-22714-1_47