一种软件自适应UML建模及其形式化验证方法

来源：软件学报杂志2015年第4期北京时间：

作者：韩德帅,杨启亮,邢建春

单位：韩德帅，解放军理工大学 国防工程学院, 江苏 南京 21000711,杨启亮，解放军理工大学 国防工程学院, 江苏 南京 210007;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21009302,邢建春，解放军理工大学 国防工程学院, 江苏 南京 21000703

摘要：软件自适应的建模和形式化验证是提高自适应软件开发效率、保证自适应软件可靠性的基础,现有研究中软件自适应可视化建模与形式化建模相隔离,一定程度上阻碍了自适应软件的开发.为此,提出MV4SAS的方法,将可视化的UML与严格化的时间自动机相结合,用于软件自适应的建模和形式化验证.首先,应用UML扩展机制引入新的构造型、标记值和约束条件,定义软件自适应建模设施,在此基础上构造软件自适应结构模型和行为模型;然后,根据定义好的转换算法将软件自适应行为模型转换为时间自动机网络,建立软件自适应形式化模型;最后,定义一组软件自适应形式化验证性质,并利用模型检测工具UPPAAL验证软件自适应模型的可靠性.案例研究表明,该方法可有效降低软件自适应建模和验证的复杂度,提高软件自适应的建模效率和模型可靠性.

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

基金资助：国家自然科学基金(61321491); 国家高技术研究发展计划(863)(2013AA01A213); 计算机软件新技术国家重点实验室(南京大学)开放课题(KFKT2014B12)