摘 要：基于自适应UMI软件开发效率提升的要求以及自适应软件可靠性的保障要求，此次研究提出了MV4SAS方法，其促进了可视化UML与严格化时间自动机的有机结合，能够实现软件自适应建模与形式化验证，首先在UML扩展机制作用下引入新的构造型、标记值以及约束条件等，在软件自适应建模设施基础上构造相应的软件自适应结构模型与行为模型，并通过转换算法实现软件自适应行为模型向时间自动机网络的转换，构建软件自适应形式化模型，对软件自适应形式化验证的性质进行定义，利用模型检测工具UPPAAL对软件自适应模型的可靠性进行验证，结果显示该方法能够在一定程度上降低软件自适应建模与验证的复杂性，提升建模效率，可靠性高，值得参考借鉴。

关键词：MV4SAS；软件自适应；UML建模；形式化验证

中图分类号：TP311.11 文献标识码：A

1 引言（Introduction）

随着现代科学技术的不断发展，我国的软件规模复杂程度及用户的需求不断加大，这也在一定程度上对软件运行、维护提出了更大的挑战[1]，在这样的发展环境下，软件自适应技术应运而生，其能够增强软件的环境适应能力，满足用户多变的需求，在运行过程中根据软件信息对相关参数、结构等进行调整，消除软件运行变化带来的消极影响，确保软件服务能力的提升，因此，对软件自适应UML建模及其形式化验证方法的研究有着重要的实践意义与应用价值。

2 预备知识概述（Summary of preliminary

knowledge）

2.1 软件自适应概念模型

作為软……