Trace Refinement in B and Event-B

TL;DR

This paper introduces BERT, a trace refinement tool for B and Event-B, enabling designers to verify behavioral preservation during model refinement, demonstrated through industrial automotive case studies.

Contribution

It presents a novel trace refinement technique and tool, BERT, specifically designed for B and Event-B methods to ensure behavioral integrity during refinement.

Findings

BERT effectively verifies trace refinement in industrial cases

The technique maintains behavioral consistency across refinement levels

Application to automotive case studies demonstrates practical utility

Abstract

Traces are used to show whether a model complies with the intended behavior. A modeler can use trace checking to ensure the preservation of the model behavior during the refinement process. In this paper, we present a trace refinement technique and tool called BERT that allows designers to ensure the behavioral integrity of high-level traces at the concrete level. The proposed technique is evaluated within the context of the B and Event-B methods on industrial-strength case studies from the automotive domain.