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

• 作者: 乌尼日其其格 吕江花 李小平 马世龙
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 类型规则 类型检查 部署方案 应用系统体系结构建模 应用系统体系结构验证
• 年，卷（期）: 2020,（8）
• 所属期刊栏目: 面向新兴系统的形式化建模与验证方法专题
• 页码范围: 2309-2335
• 页数: 27页
• 分类号: TP311
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005963

摘要

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