?url_ver=Z39.88-2004&rft_id=672&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=How+to+Interpret+Failed+Proofs+in+Event-B&rft.creator=Hoang%2C+Thai+Son&rft.subject=Event-B&rft.description=In+formal+reasoning%2C+modelling+and+proving+activities+are+closely+related.+Models+give+rise+to+different+proof+obligations+and+information+about+failed+proofs+gives+indications+on+how+models+should+be+improved.+This+document+is++an+attempt+to+address+the+latter+issue%3A+to+understand+how+to+deal+with+unprovable++obligations.+We+consider+here+proof+obligations+related+to+invariant+preservation+of+an+Event-B+model%3A+%EF%AC%81rstly%2C+to+understand+the+meaning+of+the+proof+obligations%3B+secondly%2C+to+analyse+various+ways+to+%EF%AC%81x+the+model+accordingly.+Our+analysis+is+based+on+the+concept+of+reachable+states+and+inductive+invariants.%0D%0A%0D%0AKeywords%3A+Event-B%2C+invariant%2C+inductive+invariant%2C+proof+obligations%2C+modelling+and+proving.+&rft.publisher=ETH+Zurich%2C+Switzerland&rft.date=2010-04&rft.type=Monograph&rft.type=NonPeerReviewed&rft.relation=ftp%3A%2F%2Fftp.inf.ethz.ch%2Fpub%2Fpublications%2Ftech-reports%2F6xx%2F672.pdf&rft.identifier=++Hoang%2C+Thai+Son++(2010)+How+to+Interpret+Failed+Proofs+in+Event-B.++Technical+Report.+ETH+Zurich%2C+Switzerland%2C+Zurich.++++(Unpublished)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F228%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>