基于MV4SAS研究软件自适应UML建模及其形式化验证方法研究

摘要

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