Industrial deployment of system engineering methods providing high dependability and productivity


Reasoning about Liveness in Event-B

Hoang, Thai Son and Abrial, Jean-Raymond Reasoning about Liveness in Event-B. In: ICFEM 2011, Durham, UK.

Full text not available from this repository.


Event-B is a formal method which is widely used in modelling safety critical systems. So far, the main properties of interest in Event-B are safety related. Even though some liveness properties, e.g., termination, are already within the scope of Event-B, more general liveness properties, e.g. progress or persistence, are currently unsupported. We present in this paper proof rules to reason about important classes of liveness properties. We illustrate our proof rules by applying them to prove liveness properties of realistic examples. Our proof rules are based on several proof obligations that can be implemented in a tool support such as the Rodin platform.

Item Type:Conference or Workshop Item (Paper)
Event-B > Event-B Theory
ID Code:351
Deposited By: Thai Son Hoang
Deposited On:10 Nov 2011 17:31
Last Modified:10 Nov 2011 17:31

Repository Staff Only: item control page

Deploy-Project - All right reserved