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



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 (V_ASAML) and verifiable application system architecture modelling method (V_ASAMM) are proposed. In the V_ASAML 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(T₁,T₂). In the V_ASAMM 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_ASAMS) 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.



PDF全文下载地址:

http://jos.org.cn/jos/article/pdf/5963