会议专题

ProB gets Nauty: Effective Symmetry Reduction for B and Z Models

Symmetry reduction holds great promise to counter the state explosion problem. However, currently it is conducting a life on the fringe, and is not widely applied, mainly due to the restricted applicability of many of the techniques. In this paper we propose a symmetry reduction technique applied to high-level formal specification languages (B and Z). Not only does symmetry arise naturally in most models, it can also be exploited without restriction by our method. This method translates states of a formal model into directed graphs, and then uses graph canonicalisation to detect symmetries. We use the tool NAUTY to efficiently perform graph canonicalisation, which we have interfaced with the model checker PROB.In this paper we present the general technique, show how states can be translated first into vertex-coloured graphs suitable for NAUTY. We present empirical results, showing the effectiveness of our method as well as analysing the cost of graph canonicalisation.

B-Method Tool Support Model Checking Symmetry Reduction

Corinna Spermann Michael Leuschel

Institut für Informatik, Universitat Düsseldorf Universitatsstr, 1, D-40225 Düsseldorf Institut für Informatik, Universitat Düsseldorf Universitatsstr,1,D-40225 Düsseldorf

国际会议

第二届IFIP/IEEE软件工程理论基础国际研讨会(TASE 2008)(Second IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering)

南京

英文

15-22

2008-06-17(万方平台首次上网日期,不代表论文的发表时间)