Efficient Approximate Verification of Promela Models Via Symmetry Markers

We present a new verification technique for Promela which exploits state-space symmetries induced by scalarset values used in a model. The technique involves efficiently computing a marker for each state encountered during search. We propose a complete verification method which only partially exploits symmetry, and an approximate verification method which fully exploits symmetry. We describe how symmetry markers can be efficiently computed and integrated into the SPIN tool, and provide an empirical evaluation of our technique using the TopSPIN symmetry reduction package, which shows very good performance results and a high degree of precision for the approximate method (i.e. very few non-symmetric states receive the same marker). We also identify a class of models for which the approximate technique is precise.

• Type: Conference
• Year: 2007
• Where: ATVA
• Authors: Dragan Bosnacki, Alastair F. Donaldson, Michael Leuschel, Thierry Massart
• Keywords: Approximate Verification Method, ATVA 2007, Hardware, TopSPIN Symmetry Reduction, Verification Method