Presentation
BEval is 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 the tool experiments, the two main verification strategies (manual and automatic) showed significant improvement as ProB’s evaluator proves complementary to Atelier B built-in provers. Experiments were conducted with the B model of a micro-controller instruction set; several verification conditions, that were not discharged automatically or manually with Atelier B’s provers, were automatically verified using BEval.
Credits
BEval is developped by:
- Valério Medeiros Jr. (Federal Institute of Education, Science and Technology of Rio Grande do Norte, Natal, Brazil)
- David Déharbe (Federal University of Rio Grande do Norte Department of Informatics and Applied Mathematics, Natal, Brazil)
A page on github has been set up with installation and usage instructions for BEval, as well as the download link.