Sciweavers

Share
AMAI
2010
Springer

Efficient approximate verification of B and Z models via symmetry markers

8 years 12 months ago
Efficient approximate verification of B and Z models via symmetry markers
Abstract We present a new approximate verification technique for falsifying the invariants of B models. The technique employs symmetry of B models induced by the use of deferred sets. The basic idea is to efficiently compute markers for states, so that symmetric states are guaranteed to have the same marker (but not the other way around). The falsification algorithm then assumes that two states with the same marker can be considered symmetric. We describe how symmetry markers can be efficiently computed and empirically evaluate an implementation, showing both very good performance results and a high degree of precision (i.e., very few non-symmetric states receive the same marker). We also identify a class of B models for which the technique is precise and therefore provides an efficient and complete verification method. Finally, we show that the technique can be applied to Z models as well. Keywords Model Checking
Michael Leuschel, Thierry Massart
Added 28 Feb 2011
Updated 28 Feb 2011
Type Journal
Year 2010
Where AMAI
Authors Michael Leuschel, Thierry Massart
Comments (0)
books