Symmetry reduction is a model checking technique that can help alleviate the problem of state space explosion, by preventing redundant state space exploration. In previous work, we have developed three effective approaches to symmetry reduction for B that have been implemented into the ProB model checker, and we have proved the soundness of our state symmetries. However, it is also important to show our techniques are sound with respect to standard model checking, at the algorithmic level. In this paper, we present a retrospective B development that addresses this issue through a series of B refinements. This work also demonstrates the valuable insights into a system that can be gained through formal modelling.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{TurnerBL10,
author = {Edd Turner and
Michael J. Butler and
Michael Leuschel},
editor = {Marc Frappier and
Uwe Gl{\"{a}}sser and
Sarfraz Khurshid and
R{\'{e}}gine Laleau and
Steve Reeves},
title = {A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking},
booktitle = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
{ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5977},
pages = {231--244},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-11811-1\_18},
doi = {10.1007/978-3-642-11811-1\_18},
timestamp = {Sun, 02 Jun 2019 21:23:59 +0200},
biburl = {https://dblp.org/rec/conf/asm/TurnerBL10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}