Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-75596-8_22 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
promela model,approximate method,state-space symmetry,spin tool,symmetry marker,new verification technique,approximate technique,topspin symmetry reduction package,efficient approximate verification,complete verification method,approximate verification method,empirical evaluation,state space | Discrete mathematics,Spin-½,Computer science,Theoretical computer science,Symmetry reduction,Promela,Homogeneous space | Conference |
Volume | ISSN | ISBN |
4762 | 0302-9743 | 3-540-75595-0 |
Citations | PageRank | References |
5 | 0.40 | 12 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dragan Bošnački | 1 | 113 | 7.22 |
| Alastair F. Donaldson | 2 | 661 | 52.35 |
| Michael Leuschel | 3 | 2156 | 135.89 |
| Thierry Massart | 4 | 146 | 14.17 |