高阶类型化软件体系结构建模和验证及案例

• 作者: 乌尼日其其格 吕江花 张思卿 李小平 马世龙
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 类型规则 类型检查 软件体系结构 软件体系结构建模 软件体系结构验证
• 年，卷（期）: 2019,（7）
• 所属期刊栏目: 软件形式化验证专题
• 页码范围: 1916-1938
• 页数: 23页
• 分类号: TP311
• 字数: 20303字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005749

摘要

根据权威统计数据,软件测试中发现的70％以上的错误由需求获取或体系结构设计引起.因此,应用软件体系结构在设计阶段的正确性验证非常重要.现有的软件体系结构设计方法不支持需求满足验证,需求满足验证需要其他验证工具的支持.面向主流Web应用软件的体系结构设计及其需求满足验证,提出了一种高阶类型化软件体系结构建模和验证语言(SAML)与软件体系结构建模和验证方法(SAMM).SAML语言通过定义类型和项的语法及语义,描述软件体系结构中类型和对象的构造,通过定义类型规则及其类型检查算法来判定Γ(|)-t:T和Γ(|)-R(T1,T2)是否成立.SAMM给出了软件体系结构建模范式,包括构建接口类型Mcls(type interface)、组件Mcmpt(component)、容器Mcont(container)、框Mfrm(frame)和框架Mfrwk(framework)这5层建模过程,以及生成层内与层间类型之间关系对应的类型规则,同时定义了接口类型方法调用图(GsA)用以刻画软件体系结构设计要求,定义了类型序列及其正确性用以刻画需求期望的性质,并给出了相应的验证算法.设计实现了基于该方法的原型工具系统SAMVS,其中,模型编辑环境支持应用软件的设计过程,验证环境支持设计满足需求的自动化验证.通过一个实际案例,完成了一个较大规模“互联网+”应用软件系统的体系结构建模和验证.