高阶类型化软件体系结构建模和验证及案例
作者:
作者单位:

作者简介:

乌尼日其其格(1979-),女,内蒙古赤峰人,博士,CCF学生会员,主要研究领域为软件形式化方法,类型系统;吕江花(1975-),女,博士,副教授,CCF专业会员,主要研究领域为软件形式化方法,软件工程,安全苛刻系统自动化测试;李小平(1979-),男,博士,副教授,主要研究领域为软件形式化方法,区块链;张思卿(1993-),女,硕士,主要研究领域为软件工程,软件体系结构;马世龙(1953-),男,博士,教授(研究员),博士生导师,主要研究领域为海量信息处理的计算模型,软件工程,形式化方法.

通讯作者:

吕江花,E-mail:jhlv@nlsde.buaa.edu.cn

中图分类号:

TP311

基金项目:

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


Modelling and Verification of High-order Typed Software Architecture and Case Study
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61003016, 61300007, 61305054); Base Research Foundation of Ministry of Science and Technology of China (YWF-14-JSJXY-007); Independent Discovery Foundation of State Key Laboratory of Software Development Environment of China (SKLSDE-2012ZX-28, SKLSDE-2014ZX-06)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

乌尼日其其格,李小平,马世龙,吕江花,张思卿.高阶类型化软件体系结构建模和验证及案例.软件学报,2019,30(7):1916-1938

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2018-07-10
  • 最后修改日期:2018-09-28
  • 录用日期:
  • 在线发布日期: 2019-04-03
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号