Verification of Symmetry Detection using PVS

Abstract

One of the major limitations of model checking is that of state-space
explosion. Symmetry reduction is a method that has been successfully used to alleviate
this problem for models of systems that consist of sets of identical components.
In earlier work, we have introduced a specification language, Promela-Lite, which
captures the essential features of Promela but has a fully defined semantics. We used
hand proofs to show that a static symmetry detection technique developed for this
language 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 have
not been proved mechanically to be correct, i.e., no mechanical formal verification
technique has been used to check the soundness of the approach. In this paper, we
address this issue by mechanically verifying the correctness of the symmetry detection
technique. We do this by embedding the syntax and semantics of Promela-Lite
into the theorem prover PVS and using these embeddings to both check the consistency
of syntax/semantics definitions, and interactively prove relevant theoretical
properties.