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

Temporal logic
Specifications
Formal methods
Model checking
Testing
Industry

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
Saralaya, Vikram ; Kishore, J. K. ; Reddy, Sateesh ; Pai, Radhika M. ; Singh, Sanjay. / Modeling and verification of chess game using NuSMV. Advances in Computing and Communications - First International Conference, ACC 2011, Proceedings. Vol. 191 CCIS PART 2. ed. 2011. pp. 460-470 (Communications in Computer and Information Science; PART 2).
@inproceedings{f6faa169450142b78e97db29bed7999a,
title = "Modeling and verification of chess game using NuSMV",
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.",
author = "Vikram Saralaya and Kishore, {J. K.} and Sateesh Reddy and Pai, {Radhika M.} and Sanjay Singh",
year = "2011",
doi = "10.1007/978-3-642-22714-1_47",
language = "English",
isbn = "9783642227134",
volume = "191 CCIS",
series = "Communications in Computer and Information Science",
number = "PART 2",
pages = "460--470",
booktitle = "Advances in Computing and Communications - First International Conference, ACC 2011, Proceedings",
edition = "PART 2",

}

Saralaya, V, Kishore, JK, Reddy, S, Pai, RM & 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 edn, vol. 191 CCIS, Communications in Computer and Information Science, no. PART 2, vol. 191 CCIS, pp. 460-470, 1st International Conference on Advances in Computing and Communications, ACC 2011, Kochi, India, 22-07-11. https://doi.org/10.1007/978-3-642-22714-1_47

Modeling and verification of chess game using NuSMV. / Saralaya, Vikram; Kishore, J. K.; Reddy, Sateesh; Pai, Radhika M.; Singh, Sanjay.

Advances in Computing and Communications - First International Conference, ACC 2011, Proceedings. Vol. 191 CCIS PART 2. ed. 2011. p. 460-470 (Communications in Computer and Information Science; Vol. 191 CCIS, No. PART 2).

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

TY - GEN

T1 - Modeling and verification of chess game using NuSMV

AU - Saralaya, Vikram

AU - Kishore, J. K.

AU - Reddy, Sateesh

AU - Pai, Radhika M.

AU - Singh, Sanjay

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=80051572307&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80051572307&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-22714-1_47

DO - 10.1007/978-3-642-22714-1_47

M3 - Conference contribution

SN - 9783642227134

VL - 191 CCIS

T3 - Communications in Computer and Information Science

SP - 460

EP - 470

BT - Advances in Computing and Communications - First International Conference, ACC 2011, Proceedings

ER -

Saralaya V, Kishore JK, Reddy S, Pai RM, Singh S. 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. 2011. p. 460-470. (Communications in Computer and Information Science; PART 2). https://doi.org/10.1007/978-3-642-22714-1_47