Failure Divergence Refinement for Event-B

doi:10.1007/978-3-031-98208-8_6

Return

Failure Divergence Refinement for Event-B

2026-01-01

PRE

Sebastian Stock *

Michaël Leuschel

Atif Mashkoor

DOI：10.1007/978-3-031-98208-8_6

Original

Original request for help

Save

Abstract

En 中文

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, revalidation 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.

Keywords:

Refinement

Failure traces

Event-B

Divergence

Liveness