Industrial deployment of system engineering methods providing high dependability and productivity


How to Interpret Failed Proofs in Event-B

Hoang, Thai Son (2010) How to Interpret Failed Proofs in Event-B. Technical Report. ETH Zurich, Switzerland, Zurich. (Unpublished)

Full text not available from this repository.

Official URL:


In formal reasoning, 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: to understand how to deal with unprovable obligations. We consider here proof obligations related to invariant preservation of an Event-B model: firstly, to understand the meaning of the proof obligations; secondly, to analyse various ways to fix the model accordingly. Our analysis is based on the concept of reachable states and inductive invariants. Keywords: Event-B, invariant, inductive invariant, proof obligations, modelling and proving.

Item Type:Monograph (Technical Report)
Subjects:Training > Event-B
ID Code:228
Deposited By:Thai Son Hoang
Deposited On:01 Jun 2010 12:07
Last Modified:01 Jun 2010 12:07

Repository Staff Only: item control page

Deploy-Project - All right reserved