KBX: Verified Model Synchronization via Formal Bidirectional Transformation

TL;DR

KBX addresses the challenge of maintaining rigorous consistency across multiple heterogeneous models in safety-critical systems by introducing a formal bidirectional transformation (BX) framework built on the matching logic and $\mathbb{K}$ platform. It formalizes BX as symmetric lenses, then automatically synthesizes forward ($\Gamma^{putr}$) and backward ($\Gamma^{putl}$) transformations from a unidirectional definition, using a complements holder to recover missing information and ensure round-tripping laws. A formal synchronizer combines these transformers to enable simultaneous synchronization and verification, with proofs generated in Metamath to certify model consistency. The approach is validated on industrially relevant HCSP-UML BX, achieving substantial reductions in manual specification effort (e.g., 82.8% code reduction) while delivering verification capabilities comparable to refinement-based methods, demonstrating practical impact for safety-critical system development.

Abstract

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}$.

Figures (9)

• Figure 1: Pedestrian Interaction with Traffic Signals: A depiction of a pedestrian crossing the road with a traffic light initially displaying red, followed by a 10-meter walk, button activation, a 20-second green signal, and subsequent return to red.
• Figure 2: The Architecture of KBX Formal BX Framework.
• Figure 3: A screenshot of rule1 in Fig. \ref{['fig:example']}
• Figure 4: $\mathbb{K}$ snippet for HCSP to UML unidirectional transformation of rule 1 in Fig. \ref{['fig:example-frag']}.
• Figure 5: The Detailed Synthesis Workflow of KBX Formal BX Framework.

Theorems & Definitions (10)

• definition 1: Symmetric Lens
• definition 2: Matching logic syntax
• definition 3
• definition 4
• definition 5
• definition 6
• definition 7
• definition 8
• definition 9
• definition 10