Affordable Access

Download Read

Symmetry Reduction for B by Permutation Flooding

Authors
Publisher
Springer

Abstract

Symmetry Reduction for B by Permutation Flooding Michael Leuschel1, Michael Butler2, Corinna Spermann1 and Edd Turner2 1 Institut fu¨r Informatik, Universita¨t Du¨sseldorf Universita¨tsstr. 1, D-40225 Du¨sseldorf {leuschel,[email protected] 2 School of Electronics and Computer Science, University of Southampton Highfield, Southampton, SO17 1BJ, UK {mjb,[email protected] Abstract. Symmetry reduction is an established method for limiting the amount of states that have to be checked during exhaustive model checking. The idea is to only verify a single representative of every class of symmetric states. However, computing this representative can be non- trivial, especially for a language such as B with its involved data struc- tures and operations. In this paper, we propose an alternate approach, called permutation flooding. It works by computing permutations of newly encountered states, and adding them to the state space. This turns out to be relatively unproblematic for B’s data structures and we have implemented the algorithm inside the ProBmodel checker. Empirical re- sults confirm that this approach is effective in practice; speedups exceed an order of magnitude in some cases. The paper also contains correct- ness results of permutation flooding, which should also be applicable for classical symmetry reduction in B. Keywords: B-Method, Tool Support, Model Checking, Symmetry Re- duction.1 1 Introduction The B-method [1] is a theory and methodology for formal development of com- puter systems. It is used in industry in a range of critical domains. In addition to the proof activities it is increasingly being realised that validation of the initial specification is important, as otherwise a correct implementation of an incorrect specification is being developed. This validation can come in the form of ani- mation, e.g., to check that certain functionality is present in the specification. Another useful tool is model checking, whereby the specification can be system- ati

There are no comments yet on this publication. Be the first to share your thoughts.