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

作     者：乌尼日其其格 李小平 马世龙 吕江花 张思卿 WUNIRI Qi-Qi-Ge;LI Xiao-Ping;MA Shi-Long;Lü Jiang-Hua;ZHANG Si-Qing

作者机构：软件开发环境国家重点实验室(北京航空航天大学)北京100083 鹏城实验室广东深圳518055 

基　　金：国家自然科学基金(61003016,61300007,61305054) 科技部基本科研业务费重点科技创新类项目(YWF-14-JSJXY-007) 软件开发环境国家重点实验室自主探索基金(SKLSDE-2012ZX-28,SKLSDE-2014ZX-06)~~ 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2019年第30卷第7期

页      码：1916-1938页

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

主 题 词：类型规则 类型检查 软件体系结构 软件体系结构建模 软件体系结构验证 

学科分类：08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.13328/j.cnki.jos.005749

馆 藏 号：203697698...