2024/04/29 by Jianhong Zhao, Zhao, Jianhong, Yongwang Zhao +9 · 1 citation
Computer Science · #FOS: Computer and information sciences #Model-Driven Software Engineering Techniques #Semantic Web and Ontologies #Service-Oriented Architecture and Web Services #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.2404.18771
openalex publication_date 2024/04/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 \mathbbK 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 \mathbbK 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 \mathbbK.