高阶类型化可验证应用系统体系结构建模及案例-李小平，乌尼日其其格，马世龙，吕江花.pdf
免费下载
软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2020,31(8):2309−2335 [doi: 10.13328/j.cnki.jos.005963] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563
高阶类型化可验证应用系统体系结构建模及案例
∗
李小平
1
,
乌尼日其其格
1,3
,
马世龙
1,2
,
吕江花
1
1
(软件开发环境国家重点实验室(北京航空航天大学),北京 100083)
2
(鹏城实验室,广东 深圳 518055)
3
(国家智能网联汽车创新中心,北京 100176)
通讯作者: 乌尼日其其格, E-mail: qiqige.wuniri@nlsde.buaa.edu.cn
摘 要: 随着应用软件体系结构风格变化和规模变大,其运行环境变得日趋复杂,对应用系统体系结构的设计及
其正确性验证提出了新的挑战.现有的应用系统体系结构设计关于需求满足性验证在建模与验证中需要多种工具
的支持.应用系统体系结构在设计阶段的需求满足验证,有助于客观评价应用系统部署方案和系统如期上线以及主
动运维.面向应用系统体系结构设计及其验证,在模型驱动的软件工程背景下提出一种高阶类型化可验证应用系统
体系结构建模语言(V
ASA
ML)与可验证应用系统体系结构建模方法(V
ASA
MM).V
ASA
ML 语言通过定义类型和项的语
法和语义,描述构成应用系统体系结构的类型和对象的结构,通过定义两种类型规则及其类型检查算法,判定
Γ
At:T
和
Γ
AR(T
1
,T
2
)是否成立,其中,结构类类型规则用于描述应用系统体系结构中的组成部分,关系类类型规则用于描述
组成部分之间的关系和配置.V
ASA
MM 方法给出了应用系统体系结构建模过程,包括构建 M
bd
(基本数据类型)、M
bti
(基
本接口类型)、M
dev
(设备类型)和 M
frwk
(应用系统框架)这 4 层,以及自动生成层内与层间类型之间关系对应的类型规
则,同时定义了设备类型服务调用图(G
DSI
)用以刻画部署要求,定义了类型序列及其正确性用以刻画需求期望性质,
并给出了相应的基于类型检查的验证算法.设计实现了基于该方法的原型工具系统 V
ASA
MS,其中,建模编辑环境支
持应用系统部署方案的设计过程,验证环境支持设计是否满足需求的自动验证.通过一个实际案例完成了某行业较
大规模应用系统体系结构的建模和验证.
关键词: 类型规则;类型检查;部署方案;应用系统体系结构建模;应用系统体系结构验证
中图法分类号: TP311
中文引用格式: 李小平,乌尼日其其格,马世龙,吕江花.高阶类型化可验证应用系统体系结构建模及案例.软件学报,2020,
31(8):2309−2 335. http://www.jos.org.cn/1000-9825/5963.ht m
英文引用格式: Li XP, Wuniri QQG, Ma SL, Lü JH. High-order typed verifiable application system architecture modelling and its
case. Ruan Jian Xue Bao/Journal of Software, 2020,31(8):2309−23 35 (in Chinese). http ://www.jos.org.cn/1 000-9825/5963.htm
High-order Typed Verifiable Application Sys tem Architecture Modelling and Its Case
LI Xiao-Ping
1
, WUNIRI Qi-Qi-Ge
1,3
, MA Shi-Long
1,2
, LÜ Jiang-Hua
1
1
(State Key Laboratory of Software Development Environ ment (Beihang University), Beijing 100083, Chin a)
2
(Peng Cheng Laboratory, Shenzhen 518055, Chin a)
3
(National Innovation Center of Intelli gent and Connected Vehicles, Beijing 100176, China)
∗ 基金项目: 国家自然科学基金(61305054, 61300007, 61003016); 科技部基本科研业务费重点科技创新类项目(YWF-14-JSJXY-
007)
Foundation item: National Natural Science Foundation of China (61305054, 61300007, 61003016); Basic Research Foundation of
Ministry of Science and Technology of China for Key S cientific and Technological Innovation Projects (YWF-14- JSJXY-007)
本文由“面向新兴系统的形式化建模与验证方法”专题特约编辑陈振邦副教授、冯新宇教授、刘志明教授推荐.
收稿时间: 2019-08-31; 修改时间: 2019-11-02; 采用时间: 2019-12-30; jos 在线出版时间: 2020-04-18
2310
Journal of Software 软件学报 Vol.31, No.8, August 2020
Abstra ct : 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 v erifi cation of the application system architecture needs th e support of kinds of tools. In this paper, under th e
background of MDSE (model driven software engineering), a higher-order typed verifiable application system architecture modelling
language (V
ASA
ML) and verifiable application system architecture modelling method (V
ASA
MM) are proposed. In the V
ASA
ML language,
the syntax and semantics of t ypes and terms are defined to describe the structure of th e system compositions’ types and objects, the typing
rules and its type checking algorithms are defined to pro cess the judgement of
Γ
At:T and
Γ
AR(T
1
,T
2
). In the V
ASA
MM method, the system
architecture modelling process is presented, which are the modelling of M
bd
(basic data type), M
bti
(basic interface type), M
dev
(device type),
and M
frwk
(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 (G
DSI
) 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
(V
ASA
MS) 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
appli cat ion syst em arch it ect ur e and it is w ell v erif i ed.
Key words: typing rule; type checking; deployment plan; application system architecture modelling; application system architecture
verification
随着本世纪初互联网技术和移动互联网技术的发展,应用软件的研发方法从设计、开发、测试到运维,产
生了众多理论、方法、技术和生产工具,加速了应用软件开发效率.同时,随着云计算相关技术的日渐成熟和大
数据处理与价值挖掘的需要,应用软件需求量激增,政府和服务机构日益依赖应用软件系统提高其服务质量,使
应用软件系统已成为影响国计民生的重要信息化基础设施.为了满足这些新兴需求,应用软件体系结构也从分
层、分布式的传统架构风格不断演变,逐渐发展成为面向云计算环境、基于微服务的云原生架构风格,使得由
软硬件组成的应用系统体系结构也随之变得日益复杂.在能否满足用户需求和服务质量要求方面,面临着规模
引发的复杂性挑战.美国国家标准和技术研究院 NIST(national in stitute of sta ndards a nd techn ology ),本世纪初在
一项软件测试非充分基础设施的影响分析报告中多次指出体系结构设计的重要性和在设计阶段验证需求满足
性的局限性
[1]
.应用系统体系结构设计阶段的需求满足验证问题,已成为软件工程面临的新的难题.为此,应对应
用系统体系结构进行建模并对其进行验证.
模型驱动软件工程(MDSE)主张基于模型生产软件制品
[2]
.MDSE 通常在系统建模过程中(即设计中)采用
平台无关的建模方法,在系统实现过程中采用平台相关的转换技术,发展 10 余年来,已在建模和自动代码生成
方面产生了大量灵活的、可扩展的元模型和模型转换工具
[3]
,成为了传统应用软件研发技术的一剂有效补充
[4]
,
但已有的模型驱动应用软件研发方法仍依赖多种形式化工具,才能验证应用系统体系结构设计的需求满足性,
以支持系统体系结构的改进和演化
[5]
.
基于互联网技术的应用系统中,Web 应用软件是其核心组成部分.通过将其部署于运行环境,并对运行环境
进行缜密规划和详细配置,可产生应用系统体系结构.而应用系统体系结构设计是系统上线和运维的重要基础
工作.为了提高应用系统体系结构设计质量,可参考 MDSE 中的方法和技术思路,研究可验证应用系统体系结构
建模方法.其中,研究应用系统体系结构建模是进行应用系统体系结构设计(即制定部署方案)的基础,研究应用
系统体系结构验证(即评价该方案正确性)可以将应用系统的评测提前至设计阶段,对应用系统的正常运行、满
足用户需求和服务质量要求以及系统主动运维都具有重要意义.
为了对应用系统体系结构进行更为精确的建模和更为便捷的自动验证,可以采用形式化方法进行建模和
验证.计算机科学中的形式化方法研究已有几十年的发展,其建模相关语言和方法极为丰富,其验证方法在模型
检测和定理证明两大分支上也产生了众多理论、方法和技术,并在软硬件领域被广泛应用
[6]
.模型检测通过有限
状态上的穷尽搜索反例,以期证明系统可能存在的设计缺陷,而定理证明则通过无限状态上演绎推理证明设计
的正确性.但已有的形式化方法往往需要采用多种形式化工具,例如对一些建模中采用迁移系统、自动机或
of 27
免费下载
【版权声明】本文为墨天轮用户原创内容，转载时必须标注文档的来源（墨天轮），文档链接，文档作者等基本信息，否则作者和墨天轮有权追究责任。如果您发现墨天轮中有涉嫌抄袭或者侵权的内容，欢迎发送邮件至：contact@modb.pro进行举报，并提供相关证据，一经查实，墨天轮将立刻删除相关内容。
下载排行榜
评论