The correctness of event-B inductive convergence

Anticipation proof obligations for stated variants need to be proved in Event-B even if the variant has no variable in common with an anticipated event. This often leads to models that are complicated by additional auxiliary variables and variants that need to take into account these variables. Beca...

Full description

Saved in:
Bibliographic Details
Published in:Science of computer programming 2016-12, Vol.131, p.94-108
Main Author: Hallerstede, Stefan
Format: Article
Language:English
Subjects:
Correctness
Refinement
Termination
Well-foundedness
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Anticipation proof obligations for stated variants need to be proved in Event-B even if the variant has no variable in common with an anticipated event. This often leads to models that are complicated by additional auxiliary variables and variants that need to take into account these variables. Because of such “encodings” of control flow information in the variants the corresponding proof obligations can usually not be discharged automatically. We present a new proof obligation for anticipated events that does not have this defect and prove it correct. The proof is fairly intricate due to the nondeterminism of the simulations that link refinements. An informal soundness argument suggests using a lexicographic product in the soundness proof. However, it turns out that a weaker order is required which we call quasi-lexicographic product. •An improvement of the Event-B proof obligations for anticipation and convergence.•Correctness proof for inductive convergence in Event-B using anticipation and convergence.•Introduction of new required mathematical notions, in particular, quasi-lexicographic products.
ISSN:0167-6423
1872-7964
DOI:10.1016/j.scico.2016.04.012