| 高阶类型化软件体系结构建模和验证及案例 |
| |
| 引用本文： | 乌尼日其其格,李小平,马世龙,吕江花,张思卿.高阶类型化软件体系结构建模和验证及案例[J].软件学报,2019,30(7):1916-1938. |
| |
| 作者姓名： | 乌尼日其其格 李小平 马世龙 吕江花 张思卿 |
| |
| 作者单位： | 软件开发环境国家重点实验室(北京航空航天大学), 北京 100083,软件开发环境国家重点实验室(北京航空航天大学), 北京 100083,软件开发环境国家重点实验室(北京航空航天大学), 北京 100083;鹏城实验室, 广东 深圳 518055,软件开发环境国家重点实验室(北京航空航天大学), 北京 100083,软件开发环境国家重点实验室(北京航空航天大学), 北京 100083 |
| |
| 基金项目： | 国家自然科学基金（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，其中，模型编辑环境支持应用软件的设计过程，验证环境支持设计满足需求的自动化验证.通过一个实际案例，完成了一个较大规模"互联网+"应用软件系统的体系结构建模和验证.
|
| 关 键 词： | 类型规则 类型检查 软件体系结构 软件体系结构建模 软件体系结构验证 |
| 收稿时间： | 2018/7/10 0:00:00 |
| 修稿时间： | 2018/9/28 0:00:00 |
Modelling and Verification of High-order Typed Software Architecture and Case Study |
| |
| WUNIRI Qi-Qi-Ge,LI Xiao-Ping,MA Shi-Long,L&#; Jiang-Hua and ZHANG Si-Qing.Modelling and Verification of High-order Typed Software Architecture and Case Study[J].Journal of Software,2019,30(7):1916-1938. |
| |
| Authors: | WUNIRI Qi-Qi-Ge LI Xiao-Ping MA Shi-Long L&#; Jiang-Hua and ZHANG Si-Qing |
| |
| Affiliation: | State Key Laboratory of Software Development Environment(Beihang University), Beijing 100083, China,State Key Laboratory of Software Development Environment(Beihang University), Beijing 100083, China,State Key Laboratory of Software Development Environment(Beihang University), Beijing 100083, China;Peng Cheng Laboratory, Shenzhen 518055, China,State Key Laboratory of Software Development Environment(Beihang University), Beijing 100083, China and State Key Laboratory of Software Development Environment(Beihang University), Beijing 100083, China |
| |
| Abstract: | |
| |
| Keywords: | typing rule type checking software architecture software architecture modelling software architecture verification |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
