Complex safety-critical systems require multiple models for a comprehensive description, resulting in error-prone development and laborious verification. Bidirectional transformation (BX) is an approach to automatically synchronizing these models. However, existing BX frameworks lack formal verification to enforce these models' consistency rigorously. This paper introduces KBX, a formal bidirectional transformation framework for verified model synchronization. First, we present a matching logic-based BX model, providing a logical foundation for constructing BX definitions within the $\mathbb{K}$ framework. Second, we propose algorithms to synthesize formal BX definitions from unidirectional ones, which allows developers to focus on crafting the unidirectional definitions while disregarding the reverse direction and missing information recovery for synchronization. Afterward, we harness $\mathbb{K}$ to generate a formal synchronizer from the synthesized definitions for consistency maintenance and verification. To evaluate the effectiveness of KBX, we conduct a comparative analysis against existing BX frameworks. Furthermore, we demonstrate the application of KBX in constructing a BX between UML and HCSP for real-world scenarios, showcasing an 82.8\% reduction in BX development effort compared to manual specification writing in $\mathbb{K}$.

翻译：复杂的安全关键系统需要多个模型进行完整描述，这导致开发过程易出错且验证工作繁重。双向变换（BX）是一种自动同步这些模型的方法，但现有BX框架缺乏强制执行模型一致性的形式化验证。本文提出KBX——一种用于可验证模型同步的形式化双向变换框架。首先，我们提出基于匹配逻辑的BX模型，为在$\mathbb{K}$框架内构建BX定义提供逻辑基础。其次，我们提出从单向定义合成形式化BX定义的算法，使开发者能够专注于构建单向定义，而无需关注反向同步及缺失信息的恢复。随后，我们利用$\mathbb{K}$从合成定义生成形式化同步器，用于一致性维护与验证。为评估KBX的有效性，我们将其与现有BX框架进行了对比分析。此外，我们展示了KBX在构建面向真实场景的UML与HCSP之间双向变换的应用实例，结果表明与在$\mathbb{K}$中手动编写规范相比，BX开发工作量减少了82.8%。