软件学报

作者：乌尼日其其格,李小平,马世龙,吕江花,张思卿

单位：乌尼日其其格，软件开发环境国家重点实验室(北京航空航天大学), 北京 10008311,李小平，软件开发环境国家重点实验室(北京航空航天大学), 北京 10008302,马世龙，软件开发环境国家重点实验室(北京航空航天大学), 北京 100083;鹏城实验室, 广东 深圳 51805503,吕江花，软件开发环境国家重点实验室(北京航空航天大学), 北京 10008304,张思卿，软件开发环境国家重点实验室(北京航空航天大学), 北京 10008305

关键词：类型规则;类型检查;软件体系结构;软件体系结构建模;软件体系结构验证

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

根据权威统计数据，软件测试中发现的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，其中，模型编辑环境支持应用软件的设计过程，验证环境支持设计满足需求的自动化验证.通过一个实际案例，完成了一个较大规模"互联网+"应用软件系统的体系结构建模和验证.

来源：2019年第7期

《软件学报》期刊编辑部

查看软件学报杂志2019年第7期