Automating Verification of Event-B Models
Software Engineering
2016-11-10 v1
Abstract
Event-B is one of more popular notations for model-based, proof driven specification. It offers a fairly high-level mathematical lan- guage based on FOL and ZF set theory and an economical yet expres- sive modelling notation. Model correctness is established by discharging proving a number conjectures constructed via a syntactic instantiation of schematic conditions. A large proportion of provable conjectures re- quires proof hints from a user. For larger models this becomes extremely onerous as identical or similar proofs have to be repeated over and over, especially after model refactoring stages. In the paper we briefly present a new Rodin Platform proof back-end based on the Why3 umbrella prover.
Keywords
Cite
@article{arxiv.1611.02923,
title = {Automating Verification of Event-B Models},
author = {Paulius Stankaitis and Alexei Iliasov and David Adjepon-Yamoah and Alexander Romanovsky},
journal= {arXiv preprint arXiv:1611.02923},
year = {2016}
}
Comments
Event-B day 2016, Tokyo