Trace Refinement in B and Event-B

Stock, Sebastian; Mashkoor, Atif; Leuschel, Michael; Egyed, Alexander

doi:10.1007/978-3-031-17244-1\_19

by Sebastian Stock, Atif Mashkoor, Michael Leuschel, Alexander Egyed

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.

View PDF

Reference:

Trace Refinement in B and Event-B (Sebastian Stock, Atif Mashkoor, Michael Leuschel, Alexander Egyed), In Formal Methods and Software Engineering - 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Madrid, Spain, October 24-27, 2022, Proceedings (Adrián Riesco, Min Zhang, eds.), Springer, volume 13478, 2022.

Bibtex Entry:

@Conference{DBLP:conf/icfem/StockMLE22,
  author     = {Sebastian Stock and Atif Mashkoor and Michael Leuschel and Alexander Egyed},
  booktitle  = {Formal Methods and Software Engineering - 23rd International Conference on Formal Engineering Methods, {ICFEM} 2022, Madrid, Spain, October 24-27, 2022, Proceedings},
  title      = {Trace Refinement in {B} and Event-B},
  year       = {2022},
  editor     = {Adri{\'{a}}n Riesco and Min Zhang},
  pages      = {316--333},
  publisher  = {Springer},
  series     = {Lecture Notes in Computer Science},
  volume     = {13478},
  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.},
  bdsk-url-1 = {https://doi.org/10.1007/978-3-031-17244-1%5C_19},
  doi        = {10.1007/978-3-031-17244-1\_19},
  url        = {https://doi.org/10.1007/978-3-031-17244-1\_19},
}