论文标题
B和事件B中的痕量改进
Trace Refinement in B and Event-B
论文作者
论文摘要
痕迹用于显示模型是否符合预期行为。建模者可以使用跟踪检查来确保在改进过程中保留模型行为。在本文中，我们提出了一种称为BERT的痕量改进技术和工具，该技术允许设计人员确保在混凝土级别上确保高级痕迹的行为完整性。在B和Event-B方法的背景下，对来自汽车领域的工业强度案例研究进行了评估。
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.
