Model-based System Verification: Theoretical Framework, Key Technologies, and Future Prospects

doi:10.16182/j.issn1004731x.joss.25-0797

Abstract

Abstract:

Traditional system verification methods face significant challenges in terms of efficiency, coverage, and traceability. To address these issues, this paper introduced model-based system verification (MBSV), which deeply integrated verification activities within the model-based systems engineering model system and evolution process. It presented the foundational logic of MBSV and proposed a multi-view unified verification modeling strategy based on system modeling language (SysML), integrating requirements, structure, behavior, and constraints. The paper discussed the algorithms for selecting representative paths and reducing equivalent classes to enhance verification efficiency, the principles of test path search, as well as the intelligent path search mechanism based on RL. It detailed the automated generation process for transforming abstract paths into executable test cases and discussed a dual-channel automated execution mechanism based on functional mock-up units and simulation platform SDKs to enable the seamless deployment and closed-loop feedback of verification tasks within heterogeneous simulation environments. The paper outlined future research directions for MBSV.

Key words: model-based system verification, model-based systems engineering, system modeling language, test path search, test path reduction, automated test case generation, test simulation platform, attitude determination and control system

CLC Number:

TP391

Sun Bo, Ren Yi, Wang Silin, Liu Qi, Li Zhidong. Model-based System Verification: Theoretical Framework, Key Technologies, and Future Prospects[J]. Journal of System Simulation, 2026, 38(4): 829-854.

Figures/Tables 10

Fig. 1

Fig. 2

Table 1

Terminology and notation

符号	术语/名称	形式化定义/说明
$M = (S, X, U, T, O)$	系统模型	状态集 $S$ 、可观测量 $X$ 、输入 $U$ 、状态转移 $T : S × U → S$ 、观测 $O : S → X$
$S$	状态空间	系统内部配置/变量的笛卡尔积
$X$	可观测空间	由观测映射获得的输出量
$U$	输入空间	可注入的控制/扰动变量集合
$T$	状态转移	$S k + 1 = T (s k, u k)$
$O$	观测映射	$y k = O (s k)$
$Γ$	语义映射	SysML图元 $→$ {约束，断言}的规范化映射
$G = (V, E, Λ)$	约束耦合状态图(CCSD)	顶点 $V$ 、有向边 $E$ 、边标注 $Λ (e) = (g u a r d, i n p u t_d o m a i n, a s s e r t)$
$π = (v 0, v 1, ⋯, v L)$	路径	图G上的顶点序列；可行性受守卫与输入域约束
P_cand， $P r$	候选路径集/代表性路径集	生成的全部候选路径集/经选择后的代表性路径集
$σ (π)$	路径签名	$h a s h (s t a t e_s e q, g u a r d s, a s s e r t s)$
$p G$	泛化路径	多条路径在 $R i n p$ 、 $R a s s e r t$ 达到阈值时形成的泛化路径
$R i n p$ ， $R a s s e r t$	输入域重叠率/断言一致率	$[0,1]$ 上的相似性度量
$~$	结构等价关系	$π a ~ π b ⇔ σ (π a) = σ (π b)$ 且共享关键子图
$τ u, τ a$	合并阈值	触发泛化/合并的下限
$U π$	路径可行域	$∩ e ∈ π i n p u t_d o m a i n e$
$C s t r u c t$	结构覆盖	状态/转移/判定－条件等覆盖率
$T (π)$	用例序列	$(s k, u k, α k) k = 0 L$ ，其中， $α k ⊆ Φ$
$g u a r d e$	守卫条件	使能边e的逻辑条件
$I s e q$	输入序列	来自输入空间的一系列有序输入
$S s e q$	状态轨迹	系统在特定 $I s e q$ 作用下所经历的状态序列
$ϵ a t t$	指向精度阈值	姿态指向误差RMS允许上限
$ϵ v o t e d$	冗余表决误差阈值	冗余“三取二”表决后姿态误差RMS的允许上限
$σ m a x$	最大超调量	模式切换过程中姿态指向误差的最大允许超调量
$T s e t t l e$	稳定时间上限	姿态指向误差收敛并保持在阈值内的最大允许时间
$T d e t e c t$	故障检测时间上限	FDIR从故障发生到完成识别的最大允许时间
$T u n l o a d$	卸载时间上限	动量轮从进入饱和到恢复至安全区间的最大允许时间
$H m a x$	饱和角动量阈值	判定动量轮进入饱和状态的角动量阈值
MM	动量管理子系统	Momentum Management子系统，负责监视与卸载轮系角动量

Table 1

Fig. 3

Table 2

Fig. 4

Fig. 5

Fig. 6

Fig. 7

Fig. 8

References 37

[1]	Piaszczyk C. Model Based Systems Engineering with Department of Defense Architectural Framework[J]. Systems Engineering, 2011, 14(3): 305-326.
[2]	Morkevicius A, Aleksandraviciene A, Strolia Z. System Verification and Validation Approach Using the MagicGrid Framework[J]. INSIGHT, 2023, 26(1): 51-59.
[3]	孙波, 郑凯. 数字试验测试技术研究现状、挑战与展望[J]. 系统仿真学报, 2025, 37(8): 1885-1906.
	Sun Bo, Zheng Kai. Digital Testing and Evaluation: Current Status, Challenges, and Prospects[J]. Journal of System Simulation, 2025, 37(8): 1885-1906.
[4]	Li H, Lu P. Research on Model-based Reliability Verification Technique for Civil Aircraft [C]//Proceedings of 2023 Global Reliability and Prognostics and Health Management Conference (PHM-Hangzhou). Piscataway: IEEE, 2023: 1-6. DOI: 10.1109/PHM-Hangzhou58797.2023.10482711 .
[5]	Cederbladh Johan, Cicchetti Antonio, Suryadevara Jagadish. Early Validation and Verification of System Behaviour in Model-based Systems Engineering: A Systematic Literature Review[J]. ACM Transactions on Software Engineering and Methodology, 2024, 33(3): 81.
[6]	于国斌. 深空探测任务协同的系统工程方法应用及趋势[J]. 深空探测学报(中英文), 2021, 8(4): 407-415.
	Yu Gubin. Application and Trend of Model-based Systems Engineering Methods for Deep Space Exploration Mission[J]. Journal of Deep Space Exploration, 2021, 8(4): 407-415.
[7]	Ramirez C, Thompson A. Verification and Validation Test Framework Using a Model-based Systems Engineering Approach[J]. INCOSE International Symposium, 2023, 33(1): 1091-1116.
[8]	Madni A M. MBSE Testbed for Rapid, Cost-effective Prototyping and Evaluation of System Modeling Approaches[J]. Applied Sciences, 2021, 11(5): 2321.
[9]	Tian Ye, Yin Beibei, Li Chenglong. A Model-based Test Cases Generation Method for Spacecraft Software[C]//2021 8th International Conference on Dependable Systems and Their Applications (DSA). Piscataway: IEEE, 2021: 373-382.
[10]	Bartocci Ezio, Mariani Leonardo, Nickovic Dejan, et al. Signal Feature Coverage and Testing for CPS Dataflow Models[J]. ACM Transactions on Software Engineering and Methodology, 2025, 34(7): 199.
[11]	Su Zhuo, Yu Zehong, Wang Dongyan, et al. Test Case Generation for Simulink Models Using Model Fuzzing and State Solving[C]//Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. New York: Association for Computing Machinery, 2024: 117-128.
[12]	陆涵, 张霖, 王昆玉, 等. 装备数字孪生可信评估框架研究[J]. 系统仿真学报, 2023, 35(7): 1455-1471.
	Lu Han, Zhang Lin, Wang Kunyu, et al. A Framework on Equipment Digital Twin Credibility Assessment[J]. Journal of System Simulation, 2023, 35(7): 1455-1471.
[13]	胡军, 张维珺, 李宛倩. 面向需求的安全关键系统形式化建模与验证方法研究[J]. 计算机工程与科学, 2019, 41(8): 1426-1433.
	Hu Jun, Zhang Weijun, Li Wanqian. A Requirement Oriented Formal Modeling and Verification Method for Safety Critical Systems[J]. Computer Engineering & Science, 2019, 41(8): 1426-1433.
[14]	肖思慧, 刘琦, 黄滟鸿, 等. 基于SysML的机载软件分层精化建模与验证方法[J]. 软件学报, 2022, 33(8): 2851-2874.
	Xiao Sihui, Liu Qi, Huang Yanhong, et al. Hierarchical Refined Modeling and Verification Method of Airborne Software Using SysML[J]. Journal of Software, 2022, 33(8): 2851-2874.
[15]	牛浩田, 马存宝, 韩佩, 等. 面向航电系统任务安全性的形式化建模与验证[J]. 系统工程与电子技术, 2023, 45(5): 1553-1569.
	Niu Haotian, Ma Cunbao, Han Pei, et al. Formal Modeling and Verification for Mission Safety of Avionics System[J]. Systems Engineering and Electronics, 2023, 45(5): 1553-1569.
[16]	Molnár Vince, Graics Bence, Vörös András, et al. Towards the Formal Verification of SysML v2 Models[C]//Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems. New York: Association for Computing Machinery, 2024: 1086-1095.
[17]	李彦瑞, 杨春节, 张瀚文, 等. 流程工业数字孪生关键技术探讨[J]. 自动化学报, 2021, 47(3): 501-514.
	Li Yanrui, Yang Chunjie, Zhang Hanwen, et al. Discussion on Key Technologies of Digital Twin in Process Industry[J]. Acta Automatica Sinica, 2021, 47(3): 501-514.
[18]	Löcklin Andreas, Müller Manuel, Jung Tobias, et al. Digital Twin for Verification and Validation of Industrial Automation Systems-a Survey[C]//2020 25th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA). Piscataway: IEEE, 2020: 851-858.
[19]	陶飞, 高鹏飞, 张辰源, 等. 数字试验测试验证: 理论、关键技术及应用探索[J]. 机械工程学报, 2024, 60(15): 227-254.
	Tao Fei, Gao Pengfei, Zhang Chenyuan, et al. D-ETV: Digital Experiment, Testing and Verification[J]. Journal of Mechanical Engineering, 2024, 60(15): 227-254.
[20]	杨波, 吴际, 徐珞, 等. 一种软件测试需求建模及测试用例生成方法[J]. 计算机学报, 2014, 37(3): 522-537.
	Yang Bo, Wu Ji, Xu Luo, et al. An Approach of Modeling Software Testing Requirements and Generating Test Cases[J]. Chinese Journal of Computers, 2014, 37(3): 522-537.
[21]	王鹏, 岳舒婷, 张帆, 等. 基于有限谓词追踪的民机系统需求一致性检查方法[J]. 系统工程与电子技术, 2024, 46(1): 205-218.
	Wang Peng, Yue Shuting, Zhang Fan, et al. Requirement Consistency Checking Method for Civil Aircraft Systems Based on Finite Predicate Tracing[J]. Systems Engineering and Electronics, 2024, 46(1): 205-218.
[22]	Spangelo S C, Kaslow D, Delp C, et al. Applying Model Based Systems Engineering (MBSE) to a Standard CubeSat[C]//2012 IEEE Aerospace Conference. Piscataway: IEEE, 2012: 1-20.
[23]	Cao Yue, Liu Yusheng, Qin Xujia. A Hybrid Approach to System Verification in Early Design for Complex Mechatronic Systems Based on Formal Functional Semantics[J]. Advanced Engineering Informatics, 2023, 58: 102201.
[24]	Izukura Sayaka, Yanoo Kazuo, Osaki Takao, et al. Applying a Model-based Approach to IT Systems Development Using SysML Extension[C]//Proceedings of the ACM/IEEE 14th International Conference on Model Driven Engineering Languages and Systems. Berlin: Springer Berlin Heidelberg, 2011: 563-577.
[25]	Apvrille Ludovic, Pierre de Saqui-Sannes, Hotescu Oana, et al. SysML Models Verification Relying on Dependency Graphs[C]//10th International Conference on Model-Driven Engineering and Software Development. Setúbal: Science and Technology Publications, Lda, 2022: 174-181.
[26]	Phillips I, Kenley C R. System Verification via Model-checking: A Case Study of an Autonomous Multi-differential Drive Robot[J]. INCOSE International Symposium, 2023, 17(1): 17-31.
[27]	He J, Sivanrupan G, Tsankov P, et al. Learning to Explore Paths for Symbolic Execution [C]∥ Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (CCS '21). New York: Association for Computing Machinery (ACM), 2021: 2526-2540. DOI: 10.1145/3460120.3484813 .
[28]	Khan M K. Reinforcement Learning-based Test Case Generation with Test Suite Prioritization for Android Application Testing[D]. Denton: University of North Texas, 2023.
[29]	Corradini Davide, Montolli Zeno, Pasqua Michele, et al. DeepREST: Automated Test Case Generation for REST APIs Exploiting Deep Reinforcement Learning[C]//2024 39th IEEE/ACM International Conference on Automated Software Engineering (ASE). Piscataway: IEEE, 2024: 1383-1394.
[30]	Simon Thrane Hansen, Cláudio Ângelo Gonçalves Gomes, Najafi Masoud, et al. The FMI 3.0 Standard Interface for Clocked and Scheduled Simulations[J]. Electronics, 2022, 11(21): 3635.
[31]	Hecht M, Chen J, Pugliese-Rosillo G. Verification and Validation of SysML Models[C]//2021 IEEE Aerospace Conference. Piscataway: IEEE, 2021: 1-6.
[32]	Lops A, Narducci F, Ragone A, et al. A System for Automated Unit Test Generation Using Large Language Models and Assessment of Generated Test Suites[C/OL]//2025 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). 2025: 29-36
[33]	Yang L, Yang C, Gao S, et al. On the Evaluation of Large Language Models in Unit Test Generation [C]∥ Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024). New York: Association for Computing Machinery (ACM), 2024: 1607-1619. DOI: 10.1145/3691620.3695529 .
[34]	Zhang W, Cockburn C, Henshaw M, et al. MBSE Co-Pilot: A Research Roadmap[J]. Systems Engineering, 2025, 0: 1-14.
[35]	王自力, 高鋆添, 杨德真, 等. 智能系统可靠性仿真测试与验证技术:前沿进展与挑战[J]. 系统仿真学报, 2025, 37(7): 1583-1606.
	Wang Zili, Gao Juntian, Yang Dezhen, et al. Reliability Simulation Testing and Verification Technologies for Intelligent Systems: Frontiers, Progress, and Challenges[J]. Journal of System Simulation, 2025, 37(7): 1583-1606.
[36]	Perisic Ana, Perisic Branko. Digital Twins Verification and Validation Approach Through the Quintuple Helix Conceptual Framework[J]. Electronics, 2024, 13(16): 3303.
[37]	陶飞, 马昕, 张辰源, 等. 数字试验测试验证标准体系[J]. 计算机集成制造系统, 2025, 31(1): 1-19.
	Tao Fei, Ma Xin, Zhang Chenyuan, et al. A Standard System for Digital Experiment, Testing, and Validation(D-ETV)[J]. Computer Integrated Manufacturing Systems, 2025, 31(1): 1-19.

UTP概念(OMG标准)	描述	MBSV的CCSD 等价/类比概念	映射与理由
TestCase(测试用例)	用于验证特定需求的测试过程规约	从CCSD模型生成一条完整的代表性路径	路径定义了状态和转移的序列，构成了测试过程的核心逻辑
CreateStimulusAction (创建刺激动作)	指示测试器向被测系统提交一个刺激的动作	三元组中的I	I定义了触发该状态转移的有效输入集合，功能上等同于测试刺激
ExpectResponseAction/ CheckPropertyAction	指示测试器观察一个预期响应或检查系统内部属性的动作	三元组中的A	A定义了在转移完成后必须成立的条件，代表了对系统响应或状态的预期和检查
前/后置条件 (Pre/Post Conditions)	测试步骤执行前后必须满足的逻辑条件	g充当了该测试步骤即状态转移的前置条件	g明确定义了使能该测试步骤所必需的系统状态
Verdict (判定结果：pass/fail)	对测试用例执行结果评估	在执行过程中对路径上所有A的评估结果	如果路径上所有A中的断言都成立，判定为“pass”，否则为“fail”