主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第7期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
李小平,乌尼日其其格,马世龙,吕江花.高阶类型化模型驱动的可验证应用系统体系结构建模及案例.软件学报,2020,31(8):0
高阶类型化模型驱动的可验证应用系统体系结构建模及案例
High-order Typed Model Driven Verifiable Application System Architecture Modelling and Its Case
投稿时间:2019-08-31  修订日期:2019-11-02
DOI:10.13328/j.cnki.jos.005963
中文关键词:  类型规则  类型检查  部署方案  应用系统体系结构建模  应用系统体系结构验证
英文关键词:typing rules  type checking  deployment plan  application system architecture modelling  application system architecture verification
基金项目:国家自然科学基金(61003016,61300007,61305054);科技部基本科研业务费重点科技创新类项目(YWF-14-JSJXY-007);软件开发环境国家重点实验室自主探索基金(SKLSDE-2012ZX-28,SKLSDE-2014ZX-06)
作者单位E-mail
李小平 软件开发环境国家重点实验室(北京航空航天大学), 北京 100083  
乌尼日其其格 软件开发环境国家重点实验室(北京航空航天大学), 北京 100083
国家智能网联汽车创新中心, 北京, 100176 
qiqige.wuniri@nlsde.buaa.edu.cn 
马世龙 软件开发环境国家重点实验室(北京航空航天大学), 北京 100083
鹏城实验室, 广东, 深圳 518055 
 
吕江花 软件开发环境国家重点实验室(北京航空航天大学), 北京 100083  
摘要点击次数: 600
全文下载次数: 1396
中文摘要:
      随着应用软件体系结构风格变化和规模变大,其运行环境变得日趋复杂,对应用系统体系结构的设计及其正确性验证提出了新的挑战.现有的应用系统体系结构设计无法支持需求满足验证,需求满足验证需要其它验证工具的支持.而应用系统体系结构在设计阶段的需求满足验证,有助于客观评价应用系统部署方案和系统如期上线以及主动运维.本文面向应用系统体系结构设计及其验证,在模型驱动的软件工程背景下,提出了一种高阶类型化模型驱动的可验证应用系统体系结构建模语言(VASAML)与可验证应用系统体系结构建模方法(VASAMM).VASAML语言通过定义类型和项的语法和语义,描述构成应用系统体系结构的类型和对象的结构,通过定义两种类型规则及其类型检查算法,判定Γ⊦t:T和Γ⊦RT1T2)是否成立,其中,结构类类型规则用于描述应用系统体系结构中的组成部分,关系类类型规则用于描述组成部分之间的关系和配置.VASAMM方法给出了应用系统体系结构建模过程,包括构建Mbd(基本数据类型)、Mbti(基本接口类型)、Mdev(设备类型)和Mfrwk(应用系统框架)等四层,以及自动生成层内与层间类型之间关系对应的类型规则,同时定义了设备类型服务调用图(GDSI)用以刻画部署要求,定义了类型序列及其正确性用以刻画需求期望性质,并给出了相应的基于类型检查的验证算法.设计实现了基于该方法的原型工具系统VASAMS,其中,建模编辑环境支持应用系统部署方案的设计过程,验证环境支持设计是否满足需求的自动验证.通过一个实际案例完成了某行业较大规模应用系统体系结构的建模和验证.
英文摘要:
      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 the application system architecture needs the support of other verification tools. In this paper, under the background of MDSE (Model Driven Software Engineering), a higher-order typed model driven 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 systems 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 its verification and evaluation.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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