SMC: A symmetry-based model checker for verification of safety and liveness properties

The article presents the SMC system. SMC can be used for checking safety an d liveness properties of concurrent programs under different fairness assum ptions. It is based on explicit state enumeration. It combats the state exp losion problem by exploiting symmetries of the input concurrent program, us ually present in the form of identical processes, in two different ways. Fi rstly, it reduces the number of explored states by identifying those states that are equivalent under the symmetries of the system; this is called pro cess symmetry. Secondly, it reduces the number of edges explored from each state, in the reduced state graph, by exploiting the symmetry of a single s tate; this is called state symmetry. SMC works in an on-the-fly manner; it constructs the reduced state graph as and when it is needed. This method fa cilitates early termination, speeds up model checking, and reduces memory r equirements. We employed SMC to check the correctness of, among other stand ard examples, the Link Layer part of the IEEE Standard 1394 "Firewire" high -speed serial bus protocol. SMC found deadlocks in the protocol. SMC was al so used to check certain liveness properties. A report on the case study is included in the article.