高阶类型化可验证应用系统体系结构建模及案例
作者:
作者单位:

作者简介:

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

通讯作者:

乌尼日其其格,E-mail:qiqige.wuniri@nlsde.buaa.edu.cn

中图分类号:

基金项目:

国家自然科学基金(61305054,61300007,61003016);科技部基本科研业务费重点科技创新类项目(YWF-14-JSJXY-007)


High-order Typed Verifiable Application System Architecture Modelling and Its Case
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61305054, 61300007, 61003016); Basic Research Foundation of Ministry of Science and Technology of China for Key Scientific and Technological Innovation Projects (YWF-14-JSJXY-007)

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

    随着应用软件体系结构风格变化和规模变大,其运行环境变得日趋复杂,对应用系统体系结构的设计及其正确性验证提出了新的挑战.现有的应用系统体系结构设计关于需求满足性验证在建模与验证中需要多种工具的支持.应用系统体系结构在设计阶段的需求满足验证,有助于客观评价应用系统部署方案和系统如期上线以及主动运维.面向应用系统体系结构设计及其验证,在模型驱动的软件工程背景下提出一种高阶类型化可验证应用系统体系结构建模语言(VASAML)与可验证应用系统体系结构建模方法(VASAMM).VASAML语言通过定义类型和项的语法和语义,描述构成应用系统体系结构的类型和对象的结构,通过定义两种类型规则及其类型检查算法,判定Γ|-tTΓ|-RT1T2)是否成立,其中,结构类类型规则用于描述应用系统体系结构中的组成部分,关系类类型规则用于描述组成部分之间的关系和配置.VASAMM方法给出了应用系统体系结构建模过程,包括构建Mbd(基本数据类型)、Mbti(基本接口类型)、Mdev(设备类型)和Mfrwk(应用系统框架)这4层,以及自动生成层内与层间类型之间关系对应的类型规则,同时定义了设备类型服务调用图(GDSI)用以刻画部署要求,定义了类型序列及其正确性用以刻画需求期望性质,并给出了相应的基于类型检查的验证算法.设计实现了基于该方法的原型工具系统VASAMS,其中,建模编辑环境支持应用系统部署方案的设计过程,验证环境支持设计是否满足需求的自动验证.通过一个实际案例完成了某行业较大规模应用系统体系结构的建模和验证.

    Abstract:

    As the application software's architecture style changes and its scale enlarges, the running environment of the application software turned out to be more complex than before. This prompts the verification of the application system architecture as early as in design phase to evaluate the deployment plan objectively and to contribute to the active maintenance of the system, while the existing methods of modelling and verification of the application system architecture needs the support of kinds of tools. In this paper, under the background of MDSE (model driven software engineering), a higher-order typed verifiable application system architecture modelling language (VASAML) and verifiable application system architecture modelling method (VASAMM) are proposed. In the VASAML language, the syntax and semantics of types and terms are defined to describe the structure of the system compositions' types and objects, the typing rules and its type checking algorithms are defined to process the judgement of Γ|-t:T and Γ|-R(T1,T2). In the VASAMM method, the system architecture modelling process is presented, which are the modelling of Mbd (basic data type), Mbti (basic interface type), Mdev (device type), and Mfrwk (framework type). 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 device service invocation graph (GDSI) is defined to describe the deployment requirements and the type sequences and its correctness are defined to describe the properties of user requirements, with the related verification algorithms. The prototype of the verifiable application system architecture modelling system (VASAMS) 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 an application system architecture and it is well verified.

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

李小平,乌尼日其其格,马世龙,吕江花.高阶类型化可验证应用系统体系结构建模及案例.软件学报,2020,31(8):2309-2335

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

京公网安备 11040202500063号