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模型，为在𝕂框架内构建BX定义提供逻辑基础。其次，我们提出从单向定义综合形式化BX定义的算法，使开发者能够专注于构建单向定义，而无需考虑逆向方向及同步所需的信息恢复。随后，我们利用𝕂从综合定义生成形式化同步器，用于一致性维护与验证。为评估KBX的有效性，我们与现有BX框架进行对比分析。此外，我们展示了KBX在真实场景中构建UML与HCSP之间BX的应用，与在𝕂中手动编写规范相比，BX开发工作量减少了82.8%。