Verification of Symmetry Detection using PVS - Ripon, Shamim; Miller, Alice (Electronic Communications of the EASST, 2011)
One of the major limitations of model checking is that of state-spaceexplosion. Symmetry reduction is a method that has been successfully used to alleviatethis problem for models of systems that consist of sets of identical components.In earlier work, we have introduced a specification language, Promela-Lite, whichcaptures the essential features of Promela but has a fully defined semantics. We usedhand proofs to show that a static symmetry detection technique developed for thislanguage is sound, and suitable to be used in a symmetry reduction tool for SPIN.One of the criticisms often levelled at verification implementations, is that they havenot been proved mechanically to be correct, i.e., no mechanical formal verificationtechnique has been used to check the soundness of the approach. In this paper, weaddress this issue by mechanically verifying the correctness of the symmetry detectiontechnique. We do this by embedding the syntax and semantics of Promela-Liteinto the theorem prover PVS and using these embeddings to both check the consistencyof syntax/semantics definitions, and interactively prove relevant theoreticalproperties.