Enabling analysis for Event-B

In this paper we present a static analysis to determine how events influence each other in Event-B and classical B models. The analysis, called an enabling analysis, uses syntactic and constraint-based techniques to compute the effect of executing one event on the guard of another event. We describe the foundations of the approach along with the realization in ProB. The output of the analysis can help a user to understand the control flow of a formal model. Additionally, we discuss how the information of the enabling analysis can be used to obtain a new optimized model checking algorithm. We evaluate both the performance of the enabling analysis and the new model checking technique on a variety of models. The technique can also be applied to TLA+ and Z using the ProB capabilities for translating both formalisms to classical B.