In this paper we present a static analysis to determine how events influence each other in Event-B models. The analysis, called an enabling analysis, uses syntactic and constraint-based techniques to compute the effect of executing one event on the guards of another event. We describe the foundations of the approach along with the realisation 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 optimised 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 is also applicable to B, (\mathrm{TLA}^{+}), and Z models.
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{DobrikovL16,
author = {Ivaylo Dobrikov and
Michael Leuschel},
editor = {Michael J. Butler and
Klaus{-}Dieter Schewe and
Atif Mashkoor and
Mikl{\'{o}}s Bir{\'{o}}},
title = {Enabling Analysis for Event-B},
booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 5th International
Conference, {ABZ} 2016, Linz, Austria, May 23-27, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9675},
pages = {102--118},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-33600-8\_6},
doi = {10.1007/978-3-319-33600-8\_6},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/DobrikovL16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}