 |
|
|
|
 |
 |
 |
|
 |
|
 |
|
|
| 李小平,乌尼日其其格,马世龙,吕江花.高阶类型化可验证应用系统体系结构建模及案例.软件学报,2020,31(8):2309-2335 |
| 高阶类型化可验证应用系统体系结构建模及案例 |
| High-order Typed Verifiable Application System Architecture Modelling and Its Case |
| 投稿时间：2019-08-31 修订日期：2019-11-02 |
| DOI：10.13328/j.cnki.jos.005963 |
| 中文关键词: 类型规则 类型检查 部署方案 应用系统体系结构建模 应用系统体系结构验证 |
| 英文关键词:typing rule type checking deployment plan application system architecture modelling application system architecture verification |
| 基金项目:国家自然科学基金（61305054，61300007，61003016）；科技部基本科研业务费重点科技创新类项目（YWF-14-JSJXY-007） |
|
| 摘要点击次数: 1099 |
| 全文下载次数: 1809 |
| 中文摘要: |
| 随着应用软件体系结构风格变化和规模变大，其运行环境变得日趋复杂，对应用系统体系结构的设计及其正确性验证提出了新的挑战.现有的应用系统体系结构设计关于需求满足性验证在建模与验证中需要多种工具的支持.应用系统体系结构在设计阶段的需求满足验证，有助于客观评价应用系统部署方案和系统如期上线以及主动运维.面向应用系统体系结构设计及其验证，在模型驱动的软件工程背景下提出一种高阶类型化可验证应用系统体系结构建模语言（VASAML）与可验证应用系统体系结构建模方法（VASAMM）.VASAML语言通过定义类型和项的语法和语义，描述构成应用系统体系结构的类型和对象的结构，通过定义两种类型规则及其类型检查算法，判定Γ|-t：T和Γ|-R（T1，T2）是否成立，其中，结构类类型规则用于描述应用系统体系结构中的组成部分，关系类类型规则用于描述组成部分之间的关系和配置.VASAMM方法给出了应用系统体系结构建模过程，包括构建Mbd（基本数据类型）、Mbti（基本接口类型）、Mdev（设备类型）和Mfrwk（应用系统框架）这4层，以及自动生成层内与层间类型之间关系对应的类型规则，同时定义了设备类型服务调用图（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 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. |
|
HTML 下载PDF全文 查看/发表评论 下载PDF阅读器 |
|
|
|
|
|
|
 |
|
|
|
|
 |
|
 |
|
 |
|
