by Sebastian Stock, Atif Mashkoor, Michael Leuschel, Alexander Egyed
Abstract:
Refinement guarantees that the concrete version of a model does not violate the constraints introduced at the abstract level. The peculiarity of refinement, however, is that we have no guarantee about the preservation of the behavior of the model. For example, a trace (a set of desirable states and transitions) created on the abstract model may not replay on the concrete model. Its manual recreation, usually via animation, is necessary to run the trace, as the model may have changed significantly during refinement. However, this is a labor-intensive and error-prone task. To this end, this article presents an automatic trace refining technique and tool called BERT (B and Event-B Trace Refinement Technique) that allows modelers to ensure the behavioral integrity of high-level traces at the concrete level. The cost- and time-effectiveness of BERT are shown in industrial-strength case studies from the automotive and aviation domains.
Reference:
Trace preservation in B and Event-B refinements (Sebastian Stock, Atif Mashkoor, Michael Leuschel, Alexander Egyed), In J. Log. Algebraic Methods Program., volume 137, 2024.
Bibtex Entry:
@Article{Stock2024,
author = {Sebastian Stock and Atif Mashkoor and Michael Leuschel and Alexander Egyed},
journal = {J. Log. Algebraic Methods Program.},
title = {Trace preservation in {B} and Event-B refinements},
year = {2024},
pages = {100943},
volume = {137},
abstract = {Refinement guarantees that the concrete version of a model does not violate the constraints introduced at the abstract level. The peculiarity of refinement, however, is that we have no guarantee about the preservation of the behavior of the model. For example, a trace (a set of desirable states and transitions) created on the abstract model may not replay on the concrete model. Its manual recreation, usually via animation, is necessary to run the trace, as the model may have changed significantly during refinement. However, this is a labor-intensive and error-prone task. To this end, this article presents an automatic trace refining technique and tool called BERT (B and Event-B Trace Refinement Technique) that allows modelers to ensure the behavioral integrity of high-level traces at the concrete level. The cost- and time-effectiveness of BERT are shown in industrial-strength case studies from the automotive and aviation domains.},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/jlap/StockMLE24.bib},
doi = {10.1016/J.JLAMP.2024.100943},
timestamp = {Fri, 08 Mar 2024 13:21:51 +0100},
url = {https://doi.org/10.1016/j.jlamp.2024.100943},
}