Use of rippling to automate Event-B invariant preservation proofs

Abstract

The use of formal method techniques can contribute to the production of more reliable and dependable systems. However, a common bottleneck for the industrial adoption of formal methods techniques is proof automation. To address the challenge of proof automation, we aim to improve it by using automated theorem proving techniques. We set one popular formal method technique as our working domain in this thesis, that is, Event-B. More specifically, we target a family of proofs, i.e. invariant preservation (INV) proofs, which can account for a significant part of the proofs that needs human interactions. We apply one of the most successful automated theorem proving techniques, which is rippling, to improve the proof automation of Event-B INV POs. Rippling uses metalevel guidance to automate proofs, and it is in particular useful to develop proof patches to recover proofs based on the meta-level guidance when proof attempts fail. We are especially interested in the case when lemmas are required to recover failed proofs. We combine a scheme-based theory-exploration system, i.e. IsaScheme, with rippling to develop a proof patch for lemma discovery, i.e. ahLemma. In addition to ahLemma, we also develop two proof patches to suggest case-splits and to simplify the goal and hypotheses by rewriting. The combining use of rippling and these proof patches can improve the proof automation of INV POs.