Failure divergence refinement for Event-B

TL;DR

This paper introduces failure divergence refinement semantics for Event-B to enable early validation of liveness properties, reducing re-validation effort during model refinement.

Contribution

It presents a novel failure divergence refinement approach for Event-B that preserves trace properties, along with an algorithm and tool for automatic checking.

Findings

Failure divergence refinement preserves trace properties under certain conditions.

The proposed method reduces re-validation effort in Event-B models.

The tool effectively handles sizable case studies.

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.