计算机应用研究

作者：吴润方,杜晔,黎妹红,

单位：1.北京交通大学网络空间安全学院,北京100044；2.北京交通大学唐山研究院,河北唐山063000；

关键词：UML模型,多视图一致性,结构映射,定理证明,形式化验证,

基金：中央高校基本科研业务费专项资金资助项目(2024JBZX018)；中央引导地方科技发展资金资助项目(246Z0705G)；；

针对复杂系统中UML多视图模型良构一致性验证的难题，提出了一种融合结构映射与定理证明的双层验证框架，以系统性地解决跨视图语义交织与结构耦合引发的建模质量风险。该方法通过结构映射验证算法（SMIVA）自动抽取3种视图模型间的结构匹配关系，生成良构一致性断言集以保障类型、命名与拓扑闭合性；同时，基于交互式定理证明器Coq构建形式化断言体系，将行为语义与状态迁移转换为可判定命题，实现语义一致性的逻辑推导。实验以电子商务系统为例，完成了13条良构一致性约束定理的形式化证明。结果表明，该方法能有效提升断言提取的覆盖性、自动化验证能力和验证效率，对提升UML建模质量具有重要意义。

来源：2026年第2期

《计算机应用研究》期刊编辑部

查看计算机应用研究杂志2026年第2期