loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07)
Symmetry Reduced Model Checking for B
Shanghai, China
June 06-June 08
ISBN: 0-7695-2856-2
Edd Turner, University of Southampton
Michael Leuschel, Universitat Dusseldorf Universitatsstr, Germany
Corinna Spermann, Universitat Dusseldorf Universitatsstr, Germany
Michael Butler, University of Southampton
Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric states. This paper presents a framework for symmetry reduced model checking of B machines, which verifies a unique representative from each orbit. Symmetries are induced by the deferred set; a key component of the B language. This contrasts with strategies that require the introduction of a special data type into a language, to indicate symmetry. An extended version of the graph isomorphism program, nauty, is used to detect symmetries, and the symmetry reduction package has been integrated into the PROB model checker. Relevant algorithms are presented, and experimental results illustrate the effectiveness of the method, where exponential speedups are sometimes possible.
Citation:
Edd Turner, Michael Leuschel, Corinna Spermann, Michael Butler, "Symmetry Reduced Model Checking for B," tase, pp.25-34, First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), 2007
Usage of this product signifies your acceptance of the Terms of Use.