主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2020年专刊出版计划 微信服务介绍 最新一期:2019年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
乌尼日其其格,李小平,马世龙,吕江花,张思卿.高阶类型化软件体系结构建模和验证及案例.软件学报,2019,30(7):1916-1938
高阶类型化软件体系结构建模和验证及案例
Modelling and Verification of High-order Typed Software Architecture and Case Study
投稿时间:2018-07-10  修订日期:2018-09-28
DOI:10.13328/j.cnki.jos.005749
中文关键词:  类型规则  类型检查  软件体系结构  软件体系结构建模  软件体系结构验证
英文关键词:typing rule  type checking  software architecture  software architecture modelling  software architecture verification
基金项目:国家自然科学基金(61003016,61300007,61305054);科技部基本科研业务费重点科技创新类项目(YWF-14-JSJXY-007);软件开发环境国家重点实验室自主探索基金(SKLSDE-2012ZX-28,SKLSDE-2014ZX-06)
作者单位E-mail
乌尼日其其格 软件开发环境国家重点实验室(北京航空航天大学), 北京 100083  
李小平 软件开发环境国家重点实验室(北京航空航天大学), 北京 100083  
马世龙 软件开发环境国家重点实验室(北京航空航天大学), 北京 100083
鹏城实验室, 广东 深圳 518055 
 
吕江花 软件开发环境国家重点实验室(北京航空航天大学), 北京 100083 jhlv@nlsde.buaa.edu.cn 
张思卿 软件开发环境国家重点实验室(北京航空航天大学), 北京 100083  
摘要点击次数: 933
全文下载次数: 580
中文摘要:
      根据权威统计数据,软件测试中发现的70%以上的错误由需求获取或体系结构设计引起.因此,应用软件体系结构在设计阶段的正确性验证非常重要.现有的软件体系结构设计方法不支持需求满足验证,需求满足验证需要其他验证工具的支持.面向主流Web应用软件的体系结构设计及其需求满足验证,提出了一种高阶类型化软件体系结构建模和验证语言(SAML)与软件体系结构建模和验证方法(SAMM).SAML语言通过定义类型和项的语法及语义,描述软件体系结构中类型和对象的构造,通过定义类型规则及其类型检查算法来判定Γ|-t:T和Γ|-RT1T2)是否成立.SAMM给出了软件体系结构建模范式,包括构建接口类型Mcls(type interface)、组件Mcmpt(component)、容器Mcont(container)、框Mfrm(frame)和框架Mfrwk(framework)这5层建模过程,以及生成层内与层间类型之间关系对应的类型规则,同时定义了接口类型方法调用图(GSA)用以刻画软件体系结构设计要求,定义了类型序列及其正确性用以刻画需求期望的性质,并给出了相应的验证算法.设计实现了基于该方法的原型工具系统SAMVS,其中,模型编辑环境支持应用软件的设计过程,验证环境支持设计满足需求的自动化验证.通过一个实际案例,完成了一个较大规模"互联网+"应用软件系统的体系结构建模和验证.
英文摘要:
      According to the authoritative statistics, more than 70% of software errors during the test are introduced in requirements gathering and analysis or architectural design. The design and verification of the software architecture is essential to improve the quality of application software. The existing application software design methods do not support the verification of requirements, and they usually need the support of other verification tools. In this study, with the background of Web application architecture design and verification, a software architecture modelling and verification language (SAML) and a software architecture modelling and verification method (SAMM), which are based on the higher-order type theory, are proposed. In the SAML language, the syntax and semantics of the types, the ordinary terms as well as the type terms are defined to describe the structure of types and objects, the typing rules are defined to process the judgments of Γ|-t:T and Γ|-R(T1,T2). In the SAMM method, the software architecture modelling paradigm is presented, of which is consisted of the five layers of modelling including Mcls (interface type layer), Mcmpt (component layer), Mcont (container layer), Mfrm (frame layer), and Mfrwk (framework layer). In each layer, modelling of the types and the relations of the types are needed, while the typing rules corresponding to the type relations are automatically generated. Furthermore, the method invocation graph (GSA) is defined to describe the design requirements and the type sequences and its correctness are defined to describe the properties of user requirements, and the related checking algorithms are given. The prototype of the software architecture modelling and verification system as a modelling and verifying tool is developed, to which support to the design process by modelling and the automatic verification of the design regarding to the requirements. Finally, the method is applied to a real case of large scale by the design of software architecture and its verification and evaluation.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利