BEval: A Plug-in to Extend Atelier B with Current Verification Technologies
This work addresses verification bottlenecks for users of the B method/Event-B, though it is incremental as it combines existing tools rather than introducing a fundamentally new approach.
The paper tackles the problem of limited automation in verification activities for the B method/Event-B by introducing BEval, a plug-in that integrates Atelier B with the ProB model checker. The result showed significant improvement in both manual and automatic verification strategies, with BEval automatically verifying several verification conditions that Atelier B's provers could not discharge.
This paper presents BEval, an extension of Atelier B to improve automation in the verification activities in the B method or Event-B. It combines a tool for managing and verifying software projects (Atelier B) and a model checker/animator (ProB) so that the verification conditions generated in the former are evaluated with the latter. In our experiments, the two main verification strategies (manual and automatic) showed significant improvement as ProB's evaluator proves complementary to Atelier B built-in provers. We conducted experiments with the B model of a micro-controller instruction set; several verification conditions, that we were not able to discharge automatically or manually with AtelierB's provers, were automatically verified using BEval.