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
AN - SCOPUS:80051572307
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
T2 - 1st International Conference on Advances in Computing and Communications, ACC 2011
Y2 - 22 July 2011 through 24 July 2011
ER -