From Design to Safety Analysis: Heterogeneous Model Transformation and Cross-validation
Author:
Affiliation:

Clc Number:

TP311

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    In the development of complex software systems, effective integration between the design phase and the verification phase is crucial for ensuring system reliability and functional correctness. However, heterogeneity in modeling languages, semantics, and data structures across design and verification tools often leads to semantic inconsistencies during model transformation, insufficient toolchain interoperability, and inadequate verification coverage. To address these challenges, this study proposes a layered transformation and multi-perspective cross-verification mechanism based on a unified intermediate representation (UIR). Starting from the design model, systems-theoretic process analysis (STPA) is applied to conduct hazard analysis and identify unsafe control actions, from which safety constraints are extracted and cross-checked against existing functional, timing, and safety properties. Subsequently, a mapping from the design model to the UIR is constructed, and the structure, behavior, timing, and safety constraints are formally specified within a unified syntactic and semantic domain. On this basis, layered transformation rules, together with traceability metadata, are defined to cover the above elements. Based on the UIR, complementary verification models, such as temporal, logical, and probabilistic models, are derived, and the safety constraints produced by STPA are systematically translated into verifiable properties. Multi-perspective cross-verification is then conducted, including consistency checking among source, intermediate, and target models, temporal and logical property verification, probabilistic analysis, and satisfiability checking of safety constraints. Case studies on an autonomous vehicle control system and a multi-domain collaborative unmanned aerial vehicle (UAV) control system demonstrate that the proposed method improves verification coverage and accuracy, enhances traceability throughout transformation and verification, and provides a consistent and provable technical pathway for safety-driven development of complex systems.

    Reference
    Related
    Cited by
Get Citation

吴梦丹,杨顺昆,侯展意,佘志坤,曾福萍,冀振燕.从设计到安全分析: 异构模型转换与交叉验证.软件学报,2026,37(9):3521-3556

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 08,2025
  • Revised:October 28,2025
  • Adopted:
  • Online: December 24,2025
  • Published: September 06,2026
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063