Use of rippling to automate Event-B invariant preservation proofs
View/ Open
Lin2015.pdf (1.774Mb)
Date
29/06/2015Item status
Restricted AccessEmbargo end date
31/12/2100Author
Lin, Yu Hui
Metadata
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.