KBX: Verified Model Synchronization via Formal Bidirectional Transformation

TL;DR

KBX introduces a formal framework for verified bidirectional model synchronization, leveraging logical foundations and synthesis algorithms to improve consistency and reduce development effort in safety-critical systems.

Contribution

It presents a novel KBX framework that synthesizes formal bidirectional transformations from unidirectional definitions within the $ extbf{K}$ framework, enabling verified model synchronization.

Findings

Achieved 82.8% reduction in synchronization effort.

Provided a logical foundation for BX definitions in $ extbf{K}$.

Demonstrated effective application in UML and HCSP models.

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