Trace Refinement in B and Event-B
Logic in Computer Science
2022-07-29 v1
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.
Keywords
Cite
@article{arxiv.2207.14043,
title = {Trace Refinement in B and Event-B},
author = {Sebastian Stock and Atif Mashkoor and Michael Leuschel and Alexander Egyed},
journal= {arXiv preprint arXiv:2207.14043},
year = {2022}
}