Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Failure divergence refinement for Event-B

Sebastian Stock, Michael Leuschel, Atif Mashkoor

TL;DR

This work addresses the challenge of validating liveness properties in Event-B across refinement by introducing failure divergence refinement as a semantic extension of refinement. It demonstrates that, under natural conditions, abstract traces can be preserved by refinement through $A ⊑_{fd} C$, enabling early validation of liveness without redoing work at each refinement step. A fully automatic ProB-based tool implements the algorithm, computes counterexamples when refinement fails, and supports data refinements by preventing loss of abstract behavior. The evaluation on multiple case studies (including interlocking, a Hemodialysis machine, and vending models) shows practical benefits, including debugging insights and improved refinement strategies, with implications for reducing modeling workload and enabling push-button verification of liveness properties. The work also outlines future integrations with ProB2-UI and extensions to temporal logic, broadening the scope of liveness preservation in Event-B refinements.

Abstract

When validating formal models, sizable effort goes into ensuring two types of properties: safety properties (nothing bad happens) and liveness properties (something good occurs eventually. Event-B supports checking safety properties all through the refinement chain. The same is not valid for liveness properties. Liveness properties are commonly validated with additional techniques like animation, and results do not transfer quickly, leading to re-doing the validation process at every refinement stage. This paper promotes early validation by providing failure divergence refinement semantics for Event-B. We show that failure divergence refinement preserves trace properties, which comprise many liveness properties, under certain natural conditions. Consequently, re-validation of those properties becomes unnecessary. Our result benefits data refinements, where no abstract behavior should be removed during refinement. Furthermore, we lay out an algorithm and provide a tool for automatic failure divergence refinement checking, significantly decreasing the modeler's workload. The tool is compared and evaluated in the context of sizable case studies.

Failure divergence refinement for Event-B

TL;DR

This work addresses the challenge of validating liveness properties in Event-B across refinement by introducing failure divergence refinement as a semantic extension of refinement. It demonstrates that, under natural conditions, abstract traces can be preserved by refinement through , enabling early validation of liveness without redoing work at each refinement step. A fully automatic ProB-based tool implements the algorithm, computes counterexamples when refinement fails, and supports data refinements by preventing loss of abstract behavior. The evaluation on multiple case studies (including interlocking, a Hemodialysis machine, and vending models) shows practical benefits, including debugging insights and improved refinement strategies, with implications for reducing modeling workload and enabling push-button verification of liveness properties. The work also outlines future integrations with ProB2-UI and extensions to temporal logic, broadening the scope of liveness preservation in Event-B refinements.

Abstract

When validating formal models, sizable effort goes into ensuring two types of properties: safety properties (nothing bad happens) and liveness properties (something good occurs eventually. Event-B supports checking safety properties all through the refinement chain. The same is not valid for liveness properties. Liveness properties are commonly validated with additional techniques like animation, and results do not transfer quickly, leading to re-doing the validation process at every refinement stage. This paper promotes early validation by providing failure divergence refinement semantics for Event-B. We show that failure divergence refinement preserves trace properties, which comprise many liveness properties, under certain natural conditions. Consequently, re-validation of those properties becomes unnecessary. Our result benefits data refinements, where no abstract behavior should be removed during refinement. Furthermore, we lay out an algorithm and provide a tool for automatic failure divergence refinement checking, significantly decreasing the modeler's workload. The tool is compared and evaluated in the context of sizable case studies.

Paper Structure

This paper contains 29 sections, 2 theorems, 2 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Formalization
  4. Traces in Event-B
  5. Traces and failure traces in Event-B
  6. Trace refinement
  7. Failure traces in Event-B
  8. Failure divergence refinement
  9. Trace equivalence
  10. Failure divergence checking in practice
  11. Algorithm
  12. Setup.
  13. Computation.
  14. Limitations.
  15. Evaluation
  16. ...and 14 more sections

Key Result

proposition 1

Let $A \sqsubseteq_{td} C$ and the state spaces be finite. Further, let $\sigma \in traces(A)$ and let $\Pi = \{\pi \in traces(C) \mid \tau_{C,A}(\pi) = \sigma \}$. If $\Pi \neq \mathord\varnothing$ then $\exists \pi \cdot \pi \in \Pi$ such that $last(\pi) \in stable_C$.

Figures (2)

  • Figure 1: Visualization of the state space of \ref{['lst:vending']}
  • Figure 2: Visualization of the state space of \ref{['lst:vending2']}

Theorems & Definitions (24)

  • definition 1
  • Example
  • definition 2
  • definition 3
  • Example
  • definition 4
  • definition 5
  • Example
  • definition 6
  • definition 7
  • ...and 14 more