随着本世纪初互联网技术和移动互联网技术的发展, 应用软件的研发方法从设计、开发、测试到运维, 产生了众多理论、方法、技术和生产工具, 加速了应用软件开发效率.同时, 随着云计算相关技术的日渐成熟和大数据处理与价值挖掘的需要, 应用软件需求量激增, 政府和服务机构日益依赖应用软件系统提高其服务质量, 使应用软件系统已成为影响国计民生的重要信息化基础设施.为了满足这些新兴需求, 应用软件体系结构也从分层、分布式的传统架构风格不断演变, 逐渐发展成为面向云计算环境、基于微服务的云原生架构风格, 使得由软硬件组成的应用系统体系结构也随之变得日益复杂.在能否满足用户需求和服务质量要求方面, 面临着规模引发的复杂性挑战.美国国家标准和技术研究院NIST(national institute of standards and technology), 本世纪初在一项软件测试非充分基础设施的影响分析报告中多次指出体系结构设计的重要性和在设计阶段验证需求满足性的局限性^[1].应用系统体系结构设计阶段的需求满足验证问题, 已成为软件工程面临的新的难题.为此, 应对应用系统体系结构进行建模并对其进行验证.

模型驱动软件工程(MDSE)主张基于模型生产软件制品^[2].MDSE通常在系统建模过程中(即设计中)采用平台无关的建模方法, 在系统实现过程中采用平台相关的转换技术, 发展10余年来, 已在建模和自动代码生成方面产生了大量灵活的、可扩展的元模型和模型转换工具^[3], 成为了传统应用软件研发技术的一剂有效补充^[4], 但已有的模型驱动应用软件研发方法仍依赖多种形式化工具, 才能验证应用系统体系结构设计的需求满足性, 以支持系统体系结构的改进和演化^[5].

基于互联网技术的应用系统中, Web应用软件是其核心组成部分.通过将其部署于运行环境, 并对运行环境进行缜密规划和详细配置, 可产生应用系统体系结构.而应用系统体系结构设计是系统上线和运维的重要基础工作.为了提高应用系统体系结构设计质量, 可参考MDSE中的方法和技术思路, 研究可验证应用系统体系结构建模方法.其中, 研究应用系统体系结构建模是进行应用系统体系结构设计(即制定部署方案)的基础, 研究应用系统体系结构验证(即评价该方案正确性)可以将应用系统的评测提前至设计阶段, 对应用系统的正常运行、满足用户需求和服务质量要求以及系统主动运维都具有重要意义.

为了对应用系统体系结构进行更为精确的建模和更为便捷的自动验证, 可以采用形式化方法进行建模和验证.计算机科学中的形式化方法研究已有几十年的发展, 其建模相关语言和方法极为丰富, 其验证方法在模型检测和定理证明两大分支上也产生了众多理论、方法和技术, 并在软硬件领域被广泛应用^[6].模型检测通过有限状态上的穷尽搜索反例, 以期证明系统可能存在的设计缺陷, 而定理证明则通过无限状态上演绎推理证明设计的正确性.但已有的形式化方法往往需要采用多种形式化工具, 例如对一些建模中采用迁移系统、自动机或Petri网, 而验证中采用时态逻辑公式刻画需求期望性质的方法, 使其应用规模有限^{[7, 8]}, 并不适合于大量软硬件相结合、且构成和互操作都非常复杂的应用系统体系结构建模和验证.作者所在课题组采用类型理论, 对领域数据建模和验证以及对软件体系结构建模和验证的相关工作, 说明了形式化方法在应对规模带来的复杂性方面的作用^{[9, 10]}.特别是在建模过程中自动生成类型规则, 可以更有效地支持期望性质的自动生成和验证; 同时, 在建模与验证中采用同一种形式化工具, 有助于形成统一的建模验证体系.基于类型理论, 通过类型和项的语法与语义定义、环境定义、类型规则和求值规则定义以及类型检查算法设计形成类型系统, 通过研究项的良类型和可类型化等性质进行验证.类型系统是证明论中的一类轻量级形式化工具, 也是软件编程语言的基础^[11], 因此可以更好地刻画软件的构成和功能.而应用系统体系结构中的硬件部分, 主要用于支持该体系结构中软件部分的解释和执行, 它们与软件部分的交互, 是硬件通过对外提供的接口进行的一种行为(即驱动软件行为), 因此也适合于采用类型系统进行刻画驱动软件的构成和功能.但应用系统体系结构涉及应用软件运行环境建模, 因此应用系统体系结构形式化框架不同于应用软件体系结构形式化框架^[5], 需增加平台部分的抽象和形式化描述.

本文延续建模和验证采用同一种形式化工具的思想, 在轻量级形式化方法类型系统的基础上, 面向云计算环境中的应用系统主动运维, 提出了一种高阶类型化可验证应用系统体系结构建模方法, 以期支持在设计阶段对应用系统体系结构进行需求满足验证.本文研究内容包括:一种高阶类型化可验证应用系统体系结构建模语言(verifiable application system architecture modelling language, 简称V_ASAML)、可验证应用系统体系结构建模方法(verifiable application system architecture modelling method, 简称V_ASAMM)及其验证算法和可验证建模原型系统(verifiable application system architecture modelling system, 简称V_ASAMS).为了说明该方法的有效性, 本文将该方法应用于某行业应用系统体系结构设计的实际规模应用案例中, 并给出建模与验证过程及其结果.

为此, 本文第1节综述MDSE中形式化方法在应用系统体系结构建模和验证中的研究现状.第2节定义V_ASAML语言的类型和项的语法和语义的基础上, 进一步定义两种类型规则和求值规则, 其中, 结构类类型规则用于描述应用系统体系结构中的组成部分, 关系类类型规则用于描述体系结构组成部分之间的关系和配置.第3节给出V_ASAMM方法, 包括M_bd(基本数据类型层)、M_bti(基本接口类型层)、M_dev(设备类型层)和M_frwk(应用系统体系结构层)这4层建模过程、类型序列及其正确性定义以及类型检查算法与可验证建模原型系统.第4节以某行业实际规模的应用系统部署方案的制定为背景, 给出采用V_ASAMM方法进行建模和验证的案例.第5节总结本文在建模验证方法和应用上的主要贡献.

1 相关研究

模型驱动软件工程(MDSE)的模型驱动框架(MDA)由OMG的对象管理框架发展而来, 旨在提出便捷、互操作和可重用的架构.该框架将模型划分四类, 分别为计算无关模型(CIM)、平台无关模型(PIM)、平台特定模型(PSM)和平台模型(PM)^[5], 并可以将前三者分别对应于传统应用软件研发的需求分析、设计和系统实现等三个阶段.MDA还提出了四层元模型结构, 分别为模型实例(M0)、模型(M1)、元模型(M2)和元-元模型(M3)层.其中, 元-元模型也称为元对象设施(meta object facility, 简称MOF), 提供定义元模型的标准可定义其自身, 因此置于顶层^[3].基于MDA手段的典型元模型语言是统一建模语言(UML).MDA对UML的依赖以及UML在语义上的二义性, 使得采用该语言建立模型后在验证中总是需要其他形式语义工具的辅助.MDSE的领域特定语言DSL(domain specific language)是针对领域中某些特定的问题而设计的、表达能力有限的计算机语言, 包括外部和内部DSL:外部DSL语言通常采用自定义的语法或XML语法, 需要借助有别于主编程语言的其他编译器或解释器进行处理; 内部DSL语言则通常被嵌入到主编程语言^[12].通过DSL语言配置可以在集成开发环境（如微软的Visual Studio）中利用设计模式(design pattern)和开发框架可快速地生成原型系统^{[13, 14]}.本文可验证建模方法中给出的设备类型服务调用图G_DSI可以用于刻画应用系统体系结构的设计要求, 而本文提出的可验证应用系统体系结构建模语言(V_ASAML)属于平台特定的元模型语言.

基于互联网的应用系统, 实质上是将Web应用软件部署于数据中心或云计算环境中形成的一类主要面向互联网用户的应用系统.早期Web应用软件体系结构相对简单, 其部署环境和部署过程也相对简单^[15], 然而随着行业需求和Web工程技术的不断发展, Web应用软件逐渐发展成为大规模分布式应用软件, 软件架构风格也在分布式或分层的基础上, 结合微服务架构^[16]或云原生架构等^[17], 形成了新型的软件架构风格.美国国家标准研究院NIST研究人员在其软件质量保证相关报告:在目前近1 000个公认的常见系统弱点列表CWE(common weakness enumeration)中, 有40%可在体系结构和设计阶段发现并处理, 若未能及时发现并处理, 则会大大增加修复成本^[18], 再一次说明在设计阶段进行应用系统体系结构验证的重要性.在研发方法方面, 从本世纪初的面向对象技术为主导的研发方法逐渐发展为面向组件、面向服务和模型驱动的研发方法, 出现了众多开发语言、设计模式和框架, 使得Web应用软件体系结构不仅规模变大, 构成上也变得更为复杂, 从而使得相应的应用系统体系结构规模也变得庞大而复杂^[19].此外, 随着“互联网+”理念在各行各业的渗透, 对应用系统服务质量的要求不断提高, 也对其Web应用软件的运行环境要求不断提升^[20], 特别是对云计算环境下的应用系统提出了更高的要求^[21].因此, 应用系统体系结构设计和验证面临着规模引发的复杂性挑战, 包括:1)如何设计应用系统体系结构, 并在实际部署应用软件之前验证运行环境的可连通性和可互操作性; 2)如何设计部署相关的配置, 验证应用系统体系结构性能需求的可满足性; 3)如何设计应用软件相关配置, 验证其更新部署中的兼容性; 4)如何设计部署过程, 验证其效率和对应用系统持续服务要求的可满足性.

面对上述挑战, 随着云计算技术的发展和相关支撑工具的不断成熟, 针对其中的兼容性和部署过程相关问题产生了众多实用工具和方法.研究人员提出的Nix系列部署方法及其工具^[22], 通过分析应用软件中组件之间的依赖性, 对即将部署的软件进行多级版本化管理, 通过丰富的部署策略, 可描述原子升级和降级、安全依赖和异构环境等部署要素, 实现了应用软件的安全部署和透明的字节码部署, 以期优化源文件部署中的效率、兼容性和安全问题.为了改进该方法在组件依赖性识别中相对困难的问题, 该研究团队时隔10年, 在Nix的基础上提出了支持分布式系统部署的Disnix.该方法采用声明式语言描述服务模型、基础设施模型和分发模型等3个模型, 通过增加可扩展结构和简化部署过程, 一定程度上解决了更新部署中的兼容性验证问题, 并已应用于多个实际分布式系统的部署案例^[23].随着虚拟化和容器化管理技术的迅速发展以及敏捷(agile)软件开发方法的深入应用, DevOps方法逐渐成为优化应用软件部署和集成过程的重要手段.其贡献包括两个方面:一是在管理上将应用软件开发团队和运维团队紧密结合, 提升了协作的效率; 二是在技术上将编译、持续集成、日志跟踪和监控等一系列自动化工具集协同使用, 实现了软件产品的快速交付^[24].DevOps为Web应用软件运行环境的构造提供了便捷, 为应用软件持续部署和快速迭代提供了可能, 同时, 对应用系统的主动运维和故障恢复提供了一定的技术保障^[25].但该方法本质上是一种通过缩小生产环境和开发环境之间的差距, 借助测试驱动的手段, 以期尽可能降低错误的一类方法和工具的集合.对于解决设计阶段的验证问题, 还需要引入可验证的建模技术.

为此, 可采用MDSE中的形式化建模方法进行应用系统体系结构设计, 采用形式化规约方法进行需求期望性质的刻画, 采用形式化验证方法进行设计阶段的验证.形式规约方法对传统大规模软件如美国空军航电软件、IBM中间件CICS软件以及其他商用或安全攸关等软件的代码进行了规约后, 对提高它们的软件质量效果显著; 在形式化验证方面, 多处理器如PowerScale体系结构验证中采用模型检测方法, 可将其核心算法的正确性验证缩短至几分钟; IBM的Power系列处理器的设计中大量使用了定理证明验证其正确性等众多案例表明, 形式化验证已在软硬件领域应用广泛^[7].特别是近来, 将形式化方法与前沿软件开发方法和应用系统集成与部署方法相结合成为研究热点.研究人员主张将敏捷开发方法中的测试驱动改为模型和验证驱动, 结合形式化规约和验证方法, 可以有效地降低自适应软件从需求到设计阶段的错误^[26].一种面向分布式组件动态更新的版本一致性检查方法及其工具C_ONU_P, 利用图迁移系统和模型检测, 验证了第三方应用系统的热更新^[27].云提供商亚马逊在其简单存储服务S3(simple storage service)的算法设计与开发中引入形式化方法, 利用TLA⁺语言和模型检测发现了设计阶段的错误, 并已将该方法应用于十几个实际规模系统的正确性验证中^[28].但已有的形式化方法在应用中往往需要采用多种形式化工具, 而面对上述软硬件构成的、体系结构庞杂的应用系统体系结构的设计和验证, 由于模型检测方法存在状态爆炸, 以及常规的交互式定理证明方法需要人工抽取和定义期望性质^[6]等原因, 使其难于便捷地实际应用, 因此有必要采取轻量级的形式化方法^[11].类型系统是一种轻量级的形式化方法, 其作为定理证明的一个分支, 在建模和性质规约中采用类型、类型规则和求值规则进行刻画, 在验证中利用模型中的规则, 可通过类型检查算法进行推理, 通过求值规则进行演算.在本世纪初, 有研究人员采用类型系统对软件体系结构进行了建模, 采用CSP的时态逻辑公式刻画性能需求相关的期望性质, 并验证了软件体系结构, 扩展了已有ADL语言^[29].但该方法在模型规约和性质规约中未能在同一个体系内进行, 并且仍需要人工辅助才能完成需求期望性质的抽象和定义.近来, 作者所在实验室课题组采用类型系统先后提出了领域数据和软件体系结构建模和验证方法, 通过应用于实际规模案例, 说明了形式化方法的应用规模可以进一步扩展, 通过在其支撑工具中自动生成类型规则, 说明了可以更为有效地进行形式化验证; 同时, 在建模与验证中采用同一种形式化工具, 形成了统一的建模与验证体系^{[9, 10]}.类型系统作为软件编程语言的基础^[11], 可以更好地刻画软件的构成和功能行为.而应用系统体系结构中的硬件部分, 主要用于支持该体系结构中软件部分的解释和执行, 它们与软件部分的交互, 是硬件通过对外提供的接口(驱动软件接口)进行的一种行为, 因此也适合于采用类型系统进行刻画.但前述工作仍属于平台无关的元模型语言, 不足以反映当前Web应用软件开发部署完成后可运行环境具有的多样性和异构性.为此, 有必要提出一种平台特定的元模型语言, 以期更充分地刻画数据中心或云计算环境中的应用系统体系结构.而类型系统作为定理证明中的标准工具, 使用存在量词(∃)可进一步扩展其建模能力.

本文基于上述相关研究, 在模型驱动的软件工程领域的形式化建模与验证中, 选取类型系统这一轻量级形式化方法^[11], 并在作者已有工作的基础上进一步完善高阶类型化可验证建模方法, 为在设计阶段对应用系统体系结构进行需求满足验证, 提出了本文方法.

2 V_ASAML语言

应用系统体系结构建模和验证语言(V_ASAML)包括类型和项的语法和语义定义、环境的定义、两类类型规则和求值规则的定义等几个部分组成.该语言是在领域数据建模语言^[9]及软件体系结构建模语言^[10]的基础上进行扩展而形成的建模语言, 特别是对软件体系结构建模语言SAML的类型和项使用存在量词(∃)进行扩展, 使其从平台无关的元建模语言成为平台特定的元建模语言.这一扩展的出发点在于:随着应用软件规模的不断扩大, 相比应用软件体系结构, 应用系统体系结构已经发生了质的变化.具体表现包括:1)软件体系结构的组成要素均属于软件制品范围, 而应用系统体系结构的组成要素不仅包括应用软件体系结构还包括运行环境中的硬件设备; 2)软件体系结构一经设计完成, 进入开发阶段时基本已经确定了具体的开发语言、开发框架等开发环境, 但应用系统体系结构即使设计完成, 其用于运行应用软件的基础软件如代理服务器、应用服务器以及操作系统仍具有不确定性.即应用系统体系结构设计中, 需要对此类未确定具体型号的设备进行泛化处理.为此, 本文引入了存在类型用于刻画同一应用软件所能运行的同类异构运行环境中的软硬件设备, 不仅可以提高V_ASAML语言的描述能力, 还可以在存在类型取定某个特定类型后, 使得所设计的应用系统体系结构模型成为平台相关的模型, 从而便于进行相关性质的验证.为方便阅读, 列出其所扩展的定义.

2.1 类型和项的语法

用符号T表示任意类型, 类型T在已有基础上扩展了存在类型, 如下所示.

$ T::=T\left| X \right|\left\{ l:T \right\}\left| {{T}^{*}} \right|\left\{ T \right\}\left| {{T}_{i}}+{{T}_{j}} \right|{{T}_{i}}\times {{T}_{j}}\left| {{T}_{j}}\to {{T}_{j}} \right|\left\{ {{T}_{1}}, \ldots , {{T}_{k}} \right\}\text{ }\!\!|\!\!\text{ }\left\{ \exists X, T \right\}. $

其中, X为类型变量, T, T_i, T_j均为类型.{∃X, T}称为存在类型, 表示对{∃X, T}中的一个元素t, 对某个类型S, t是类型[X↦S]T的值^[11].存在类型{∃X, T}可以用于定义接口类型.

V_ASAML语言中, 项也分为两种, 其中不含类型变量的项称为一般项(ordinary term), 记为t^ord; 含有类型变量或类型常量的项称为类型项(type term), 记为t^type.

(1) t^ord定义如下.

$ \begin{align} & {{t}^{ord}}::=error|x|c|\{l={{t}^{ord}}\}|(t_{1}^{ord}, ..., t_{n}^{ord})|\text{ }f(t_{1}^{ord}, ..., t_{n}^{ord})|\lambda x:{{T}_{i}}.{{t}^{ord}}:{{T}_{j}}|{{t}^{ord}}(u)|{{t}^{ord}}\text{ as }T| \\ & \text{ if }t_{i}^{ord}\text{ then }t_{j}^{ord}\text{ else }t_{k}^{ord}|\text{try }t_{i}^{ord}\text{ with }t_{j}^{ord}. \\ \end{align} $

其中, x, c和error均为原子项分别表示变量符号、常量符号和异常项.

(2) t^type定义如下.

$ {{t}^{type}}::=\\X\left| C \right|T\to T\left| \left\{ \exists X, T \right\} \right|\left\{ *{{T}_{i}}, {{v}^{type}} \right\}\ \text{as}\ {{T}_{j}}\left| {{t}^{type}}\left[ T \right] \right|\left\{ {{\left[ \exists X \right]}^{*}}\left\{ {{\left[ l:X \right]}^{*}}, {{\left[ l:T \right]}^{*}}, methods:\left\{ \left[ l:T\to T \right] \right\} \right\} \right\}, |\lambda X.{{t}^{type}}:T. $

其中, X和T分别表示类型变量符号和类型常量符号^[11].

本文t^ord的定义与SAML^[10]中t^o的定义一致, 类型项t^type的定义在SAML^[10]中t^t的基础上进行扩展, 使用了存在量词(∃).为方便, {[∃X]^*, {[l:X]^*, [l:T]^*, methods:{[l:T→T]^*}}}记为T^(∃)intf, 称为泛化接口类型, 实为带存在量词接口类型, 其中, l, methods和[A]^*分别表示标签和序列.一组带标签的映射类型构成了泛化接口类型的一组方法.泛化接口类型也对应抽象数据类型系统^[30].以T^(∃X)intf={∃X, {state:X, methods:{get:X→Nat, inc:X→X}}}为例, 是一个泛化接口类型, 若将T^(∃X)intf中的存在类型的类型变量X取定为Nat(自然数类型), 则T^(∃X)intf中存在量词可被消去, 且get和inc方法是自然数类型到自然数类型的映射, T^(∃X)intf类型变量取定后成为计数器接口类型.

2.2 环境的定义

环境Γ是变量绑定的序列, 对V_ASAML语言, 可定义为Γ::=Ø|Γ, t^ord:T|Γ, t^type:T|Γ, X.一个非空的环境Γ可被递归定义为$t_{1}^{ord}:{{T}_{1}}, ..., t_{n}^{ord}:{{T}_{n}}, t_{1}^{type}:{{T}_{k}}, ..., t_{m}^{type}:{{T}_{m}}, n, m, k\ge 1$, 其中, $t_{i}^{ord}(n\ge i\ge 1)$为一般项, $t_{j}^{type}\text{(}m\ge j\ge k\text{)}$为类型项.

2.3 类型和项的语义

本文类型的语义定义与SAML^[10]的部分一致, 新增存在类型部分定义如下:

设||T||表示类型T的值域, 则V_ASAML语言中存在类型的语义为:||{∃X, T}||=forall S, ||[X↦S]T||.其中, Γ⊢S, 即S是环境Γ中的一个类型, 该语义集合等式表示.若t是||{∃X, T}||中的一个元素, 则存在某个类型S, t是类型[X↦S]T的值^[11].

V_ASAML语言中新增类型项t^type的语义如下.

$ \begin{align} & ||{{T}^{(\exists X)intf}}||=||\{{{[\exists X]}^{*}}, \{{{[l:X]}^{*}}, {{[l:T]}^{*}}, methods:\{{{[l:T\to T]}^{*}}\}\}\}|| \\ & \text{ }=\underset{\Gamma \vdash S}{\mathop{{{\cup }^{+}}}}\, ||\{{{[l:S]}^{*}}, {{[l:[X\mapsto S]T]}^{*}}, methods:\{{{[l:[X\mapsto S]T\to [X\mapsto S]T]}^{*}}\}\}||. \\ \end{align} $

其中, ∪⁺表示集合的和, 例如, A∪⁺B=A+B, 其中, A和B是集合, 它可以对应一个抽象数据类型系统^[30].

在上下文环境清楚时, 可将项t^ord和t^type简写为t, 其值可以简写为v.

2.4 求值规则和类型规则

求值规则方面, V_ASAML语言的求值规则与SAML语言的求值规则一致^[10].

V_ASAML语言的类型规则用于判定在环境Γ中, Γ⊢t:T是否成立.其中, t可以是项t^ord或t^type, 类型规则仍划分为结构类规则和关系类规则.应用系统体系结构中的组成部分可以采用结构类类型规则描述, 而组成部分之间的关系和配置可以采用关系类类型规则描述.

因引入存在量词而新增的结构类规则如下.

$ $\begin{matrix} \frac{{{t}_{2}}:[X\to U]{{T}_{2}}}{{{\{}^{*}}U, {{t}_{2}}\}\text{ as }\{\exists X, {{T}_{2}}\}:\{\exists X, {{T}_{2}}\}}(\text{TR}6)\text{, } \\ \frac{{{({{t}_{1}}:X)}^{*}}, {{(x:X)}^{*}}, {{({{T}_{1}}\to {{T}_{2}})}^{*}}, {{((\lambda y:{{T}_{1}}.{{t}_{2}}):{{T}_{2}})}^{*}}, {{T}^{(\exists X)intf}}=\{{{[\exists X]}^{*}}, \{{{[l:X]}^{*}}, {{[l:T]}^{*}}, methods:\left\{ {{[l:T\to T]}^{*}} \right\}\}\}\text{ }}{\text{ }\{{{({{(}^{*}}T))}^{*}}, \{{{(x={{t}_{1}})}^{*}}, methods:\{{{((l=\lambda y:{{T}_{1}}.{{t}_{2}}):{{T}_{2}})}^{*}}\}\}\}:{{T}^{(\exists X)intf}}}(\text{TR}7)\text{, } \\ \end{matrix}$ $

其中, 类型规则(TR7)体现了泛化接口类型的构造规则.

由于引入存在类型而扩展的关系类类型规则的定义如下.

(1) 泛化接口类型方法关联关系:如果T^(∃)intf为泛化接口类型, 且T^(∃)intf={[∃X]^*, {[l:X]^*, [l:T]^*, methods:{[l:T₁→T₂]^*}}}, 则其中的方法(带标签的映射类型)l:T₁→T₂与T^(∃)intf方法关联, 记为$(l:{{T}_{1}}\to {{T}_{2}})\xrightarrow{methods}{{T}^{(\exists )intf}}$.

(2) 泛化接口类型成员类型关联关系:如果T^(∃)intf为泛化接口类型, 且T^(∃)intf={[∃X]^*, {[l:X]^*, [l:T]^*, methods:{[l:T→T]^*}}}, 则其中的类型(带标签的类型变量或类型)l:X和l:T与T^(∃)intf成员类型关联, 记为$l:X\xrightarrow{member}{{T}^{(\exists )intf}}$和$l:T\xrightarrow{member}{{T}^{(\exists )intf}}$.

(3) 泛化关联关系:如果T^(∃)intf为泛化接口类型, 且T^(∃)intf={[∃X]^*, {[l:X]^*, [l:T]^*, methods:{[l:T→T]^*}}}, T^intf为T^(∃)intf中的类型变量X取定后的接口类型, 则T^intf和T^(∃)intf之间存在泛化关联关系, 记为

$ {{T}^{intf}}\xrightarrow{generalize}{{T}^{(\exists X)intf}}\text{.} $

其对应的类型规则公式如下.

$ \begin{matrix} \frac{\text{ }\Gamma \vdash {{T}_{1}}, \Gamma \vdash {{T}_{2}}, {{T}^{(\exists X)intf}}=\{{{[\exists X]}^{*}}, \{{{[l:X]}^{*}}, {{[l:{{T}_{1}}]}^{*}}, {{[l:{{T}_{2}}]}^{*}}, methods:\{{{[l:{{T}_{1}}\to {{T}_{2}}]}^{*}}\}\}\}, I=l:{{T}_{1}}\to {{T}_{2}}}{(l:{{T}_{1}}\to {{T}_{2}})\xrightarrow{methods}{{T}^{\left( \exists X \right)\operatorname{int}f}}}(TR16) \\ \frac{\Gamma \vdash X, \Gamma \vdash {{T}_{1}}, \Gamma \vdash {{T}_{2}}, {{T}^{(\exists X)intf}}=\{{{[\exists X]}^{*}}, \{{{[l:X]}^{*}}, {{[l:{{T}_{1}}]}^{*}}, {{[l:{{T}_{2}}]}^{*}}, methods:\{{{[l:{{T}_{1}}\to {{T}_{2}}]}^{*}}\}\}\}}{l:X\xrightarrow{member}{{T}^{(\exists X)intf}}, l:{{T}_{1}}\xrightarrow{member}{{T}^{(\exists X)intf}}, l:{{T}_{2}}\xrightarrow{member}{{T}^{(\exists X)intf}}}(TR17) \\ \frac{{{T}^{(\exists X)intf}}=\{{{[\exists X]}^{*}}, \{{{[l:X]}^{*}}, {{[l:T]}^{*}}, methods:\{{{[l:T\to T]}^{*}}\}\}\}, {{T}^{intf}}=\{{{[l:T]}^{*}}, methods:\{{{[l:T\to T]}^{*}}\}\}}{{{T}^{intf}}\xrightarrow{generalize}{{T}^{(\exists X)intf}}}(TR17) \\ \end{matrix} $

关于关系类规则TR16举例如下:若某一个泛化接口类型$T_{3}^{\left( \exists X \right)intf}=UserInterfaceService$的方法集里包含一个成员M₁₁=pingcmd:IPAddress→PingResult为带标签的映射类型, 该类型与$T_{3}^{\left( \exists X \right)intf}$具有方法关联关系${{M}_{11}}\xrightarrow{methods}T_{3}^{\left( \exists X \right)intf}$.

2.5 类型检查算法

基于上述结构类类型规则和关系类类型规则设计类型检查算法.类型检查算法用以判断Γ⊢t:T和Γ⊢R(T₁, T₂)是否为真.前者判定对任意输入的一个项t, 判定能否类型化为T; 后者判定对于任意输入的两个类型T_i和T_j, 判定它们之间是否存在期望的关系.本文对SAML已有算法TCA和RCA进行了重写和接口参数优化.

TCA算法的递归验证过程中, 不仅输入给定项t, 还输入环境Γ中已构造的类型规则集合和类型集合以提高算法健壮性.该算法伪代码如下.

算法1.TCA(·).

Input:t_.length≥1, S_TypeRules≠Ø, S_Types≠Ø.

1.    matchedFlag←false; type←undefined; trlen←S_TypeRules.length

2.    for(i=0 to trlen) do

3.      if (TR_i∈S_TypeRules) and (θ(t)=θ(TR_i.denominator.term)) then //θ是合一算法unify的输出^[11]

4.        if TR_i.numerator≠Ø then //判断TR_i是否存在分子

5.          nlen←TR_i.numerator.term.length;

6.          for(k=1 to nlen) do

7.            θ(t_k)←θ(TR_i.numerator.term); r_k←TCA(θ(t_k), S_TypeRules, S_Type);

8.            matchedFlag←matchedFlag∧(r_k.type∈S_Types)

9.          end for

10.        else //若TR_i没有分子

11.          matchedFlag←true; break;

12.        end if

13.      end if

14.    end for

15.    if (matchedFlag=false) then

16.      type←t:Undefined;

17.    else

18.      (type←TR_i.denominator.type)∈S_Types

19.    end if

Output:t:type.

RCA算法的递归验证过程中, 不仅输入给定两个类型T_i和T_j, 还输入环境Γ中已构造的类型规则集合和类型集合以提高算法健壮性.且当某条规则TR_m分母通过合一代换得到匹配, 则在检查分子时, 考虑了某一个项t_k作为条件之一的可能性.即每一个前提C_k(t_k, T_1k, T_2k)的或者形如t_k或者形如R_k(T_1k, T_2k)).若所有的t_k均能够类型化或R_k(T_1k, T_2k)均得到满足, 说明R(T₁, T₂)可以确定, 并且属于S_Relational.该算法伪代码如下.

算法2.RCA(·).

Input:R(T_i, T_j), S_Relational≠Ø, S_Types≠Ø.

1.  satisfiedFlag←false; relation←undefined; rellen←S_Relational.length;

2.  for (i=0 to relen) do

3.    if R(θ(T_i), θ(T_j))=θ(TR_m.denominator) then

4.      if TR_m.numerator≠Ø then //判断TR_m是否存在分子

5.        nlen←TR_m.numerator.term.length

6.        for (k=1 to nlen) do

7.          C_k←TR_m.numerator.term_k;

8.          if (C_k≈t_k) then

9.            r_k←TCA(θ(t_k), S_TypeRules, S_Type); //θ是合一算法unify的输出^[11]

10.            satisfiedFlag←satisfiedFlag∧(result_k∈S_Relational);

11.          else if (C_k≈R_k(T_ik, T_jk)) then

12.            result_k←RCA(R_k(θ(T_ik), θ(T_jk)), S_Relational, S_Types);

13.            satisfiedFlag←satisfiedFlag∧(result_k.relation∈S_Relational);

14.          end if

15.        end for

16.      else //若TR_m没有分子

17.        satisfiedFlag←true; break;

18.      end if

19.    end if

20.  end for

21.  if (satisfiedFlag=false) then

22.    relation←undefined;

23.  else

24.    relation←TR_i.denominator;

25.  end if

Output:relation.

基于TCA和RCA算法设计的类型序列正确性的检查算法可以用于判定所构建的类型系统是否满足类型关系集合R所表示的期望性质.为全文完整性, 列出其算法流程如下.

算法3. CheckCorrectness(·).

Input:${T_1};...;{T_m}_{\{ {R_1}, ..., {R_k}\} }$, m≥1, k≥0.

1.  flag←false; decision←incorrect;

2.  for (i=0 to k)

3.    R_i←R(T_j, T_k)

4.    if T_k; T_l⊂T₁; …; T_m then

5.      relation←RCA(R_i(T_j, T_k), S_Relational, S_Types);

6.      if (relation≠Undefined) then

7.        flag←(relation∈S_Relational);

8.      else

9.        flag←false; break;

10.      end if

11.    end if

12.  end for

13.  if (f=true) then decision←correct;

14.  end if

Output: result.

基于类型之间关系的类型序列正确性判定的问题可归结为项的类型化判定(即判定Γ⊢t:T是否成立).

3 V_ASAMM方法 3.1 基于建模范式的应用系统体系结构模型

本文对V_ASAML中的类型细分为基本数据类型、基本接口类型、设备类型和应用系统体系结构类型, 其中, (1)基本数据类型为应用给定的有限多个类型, 例如IPAddress、Context、URI、UserAgent、cookie、ConfigFile、Script、ServerName、TCPPacket等; (2)基本接口类型为接口类型或泛化接口类型; (3)设备类型为由有限多个基本接口类型聚合的乘积类型, 一个应用系统体系结构中的软件设备和硬件设备都可以统一归结为设备类型; (4)应用系统体系结构类型为由有限多个设备类型聚合的乘积类型, 一个应用系统体系结构可以由多个软件设备或硬件设备聚合而成, 软硬件之间通过接口调用或协同, 形成应用系统体系结构.因此, 应用系统体系结构建模方法从底向上包括M_bd(基本数据类型), M_bti(基本接口类型), M_dev(设备类型)和M_frwk(应用系统体系结构类型)等4层.各个层上的建模包括定义本层内的类型和类型关系以及相邻层之间的类型关系.

下面给出应用系统体系结构建模范式相应的公式, 其中R表示所有关系对应的类型规则集合, M_bd称为基本数据类型层, M_bti称为基本接口类型层, M_dev称为设备类型层, M_frwk称为应用系统体系结构层.

$ \begin{array}{l} {M_{bd}} = \left\{ {\begin{array}{*{20}{l}} {{T_1}, ..., {T_i}, ..., {T_m}, {\rm{ }}1 \le i \le m}\\ {{R_i}({T_j}, {T_k})|{R_i} \in R, {\rm{ }}1 \le i \le {L_{bd}}, 1 \le j, k \le m} \end{array}} \right\}\\ {M_{bti}} = \left\{ {\begin{array}{*{20}{l}} {T_1^{(\exists X)intf}, ..., T_n^{(\exists X)intf}|T_j^{(\exists X)intf} = \{ {{[\exists X]}^*}, \{ {{[l:X]}^*}, {{[l:{T_1}]}^*}, {{[l:{T_2}]}^*}, methods:\{ {{[l:{T_1} \to {T_2}]}^*}\} \} \} , {\rm{ }}1 \le j \le n}\\ {{R_i}(T_j^{(\exists X)intf}, T_k^{(\exists X)intf})|{R_i} \in R, {\rm{ }}1 \le i \le {L_{bti}}_{_1}, 1 \le j, k \le n}\\ {{R_j}(T_i^{(\exists X)intf}, {T_k})|{R_j} \in R, {\rm{ }}1 \le j \le {L_{bti}}_{_2}, 1 \le i \le n, 1 \le k \le m} \end{array}} \right\}\\ {M_{dev}} = \left\{ {\begin{array}{*{20}{l}} {{D_1}, ..., {D_x}, , {D_i} = \{ T_{i1}^{(\exists X)intf}, ..., T_{ik}^{(\exists X)intf}\} , {\rm{ }}1 \le i \le x, 1 \le k \le n{\rm{ }}}\\ {{R_i}({D_j}, {D_k})|{R_i} \in R, {\rm{ }}1 \le i \le {L_{dev}}_{_1}, 1 \le j, k \le x}\\ {{R_j}({D_i}, T_k^{(\exists X)intf})|{R_j} \in R, {\rm{ }}1 \le j \le {L_{dev}}_{_2}, 1 \le i \le x, 1 \le k \le n} \end{array}} \right\}\\ {M_{frwk}} = \left\{ {\begin{array}{*{20}{l}} {AF{W_1}, ..., AF{W_v}, , AF{W_i} = \{ {D_{i1}}, ..., {D_{ik}}\} , {\rm{ }}1 \le i \le v, 1 \le k \le x}\\ {{R_{ij}}(AF{W_i}, {D_k})|{R_{ij}} \subseteq R, {\rm{ }}1 \le j \le {L_{frwk}}, 1 \le i \le v, 1 \le k \le x} \end{array}} \right\} \end{array} $

定义1(应用系统体系结构模型).设M=M_bd∪M_bti∪M_dev∪M_frwk, 那么M称为应用系统体系结建模范式(application system architecture modelling paradigm), 是一个类型系统.其中, M_frwk为一个应用该系统体系结构元模型, AFW∈M_frwk为一个应用系统体系结构模型.

构造M_bd, M_bti, M_dev和M_frwk的过程称为应用系统体系结构建模过程, 其具体示意如图 1所示.

图 1给出了建模范式包括4个部分, 分别为:(1)基本数据类型建模, 包括应用系统体系结构模型中的所有基本数据类型T₁, …, T_m, m≥1, 其构成第1层; (2)基本接口类型建模, 包括应用系统体系结构模型中的所有基本接口类型, $T_1^{(\exists X)intf}, ..., T_n^{(\exists X)intf}$, n≥1, 它们构成第2层; (3)设备类型建模, 包括应用系统体系结构模型中的所有设备类型D₁, …, D_x, x≥1, 它们构成第3层; (4)应用系统体系结构框架建模, 包括应用系统体系结构框架AFW₁, …, AFW_v, v≥1, 它们构成第4层.

应用系统体系结构模型中存在如图 1中连线所示的关系:M_bd层内的^{-out/《param》→}表示存在输出参数关联关系, ^{-in/《param》→}表示存在输入参数关联关系; M_bd与M_bti层间的^-methods→表示存在方法关联关系; M_bti与M_dev以及M_dev与M_frwk层间的表示存在聚合关系; 而M_bti和M_dev层内存在服务可调用关系.最终, M是否满足部署需求则由应用系统体系结构中各层类型的定义及其关系决定.

应用系统体系结构模型中软硬件接口之间的相互可调用或协同, 主要体现为上述M_bti和M_dev两层的层内类型之间可调用关系.其中, M_bti层内的可调用关系定义如SAMM^[10]中的类型规则定义.为方便, 本文列出其类型规则, 见表 1.

设备类型层M_dev的层内存在可调用关系和可连通关系.

定义2(设备类型服务可调用关系).设有两个基本接口类型$T_1^{(\exists X)intf}, T_2^{(\exists X)intf}$分别属于两个设备类型D₁, D₂, 即$T_1^{(\exists X)intf} = {D_1}.i, T_2^{(\exists X)intf} = {D_2}.j$, 并且若接口类型$T_2^{(\exists X)intf}$可调用接口类型$T_1^{(\exists X)intf}$, 则其所属的设备类型之间通过指定的服务可调用, 记为${{D}_{2}}\xrightarrow{invocable(T_{2}^{(\exists X)intf}, T_{1}^{(\exists X)intf})}{{D}_{1}}$.

其类型规则为

$ \frac{T_{1}^{(\exists X)intf}, T_{2}^{(\exists X)intf}, T_{1}^{(\exists X)intf}={{D}_{1}}.i, T_{2}^{(\exists X)intf}={{D}_{2}}.j, T_{2}^{(\exists X)intf}\xrightarrow{invocable\left( {{I}_{2}}, {{I}_{1}} \right)}T_{1}^{(\exists X)intf}}{{{D}_{2}}\xrightarrow{incokable(T_{2}^{(\exists X)intf}, T_{1}^{(\exists X)intf})}{{D}_{1}}}(\text{TR}22). $

定义3(设备类型可连通关系).若T为设备连通相关接口类型, 则两个设备类型D₁和D₂可连通, 当且仅当T < :D₁且T < :D₂, 记为${{D}_{1}}\overset{linkable}{\longleftrightarrow}{{D}_{2}}$(或〈D₁|D₂〉_T).

其类型规则为

$ \frac{T, T_{1}^{(\exists X)intf}, T_{2}^{(\exists X)intf}, T_{1}^{(\exists X)intf}={{D}_{1}}.i, T_{2}^{(\exists X)intf}={{D}_{2}}.j, T<:{{D}_{1}}, T<:{{D}_{2}}}{{{D}_{1}}\overset{linkable}{\longleftrightarrow}{{D}_{2}}}(\text{TR}23). $

M_dev层中, 设备类型之间的可连通关系是设备类型互操作的基础.设备类型服务可调用关系及其实际可调用关系合起来用于描述设备类型之间的互操作性.

3.2 基于设备类型服务调用图的需求分析

本文建模范式的4个层次中, 应根据应用系统体系结构设计要求对M_bti和M_dev两层层内的可调用关系进行建模.该设计要求的制定源于应用系统部署需求.与SAMM类似地, 采用一个有向图G_DSI表示设备以及基本接口类型中方法之间的调用关系, 刻画实际设计要求, 如定义4所示.

定义4(设备类型服务调用图G_DSI).有向图G_DSI是$\{{{S}^{{{T}^{(\exists X)intf}}}}, {{S}^{M}}, {{S}^{entry}}, {{S}^{terminate}}, R\}$形式的五元组, 且

(1)    ${{S}^{{{T}^{(\exists X)intf}}}}$表示图中泛化接口类型集合;

(2)    S^M表示图中所有顶点集合, 对于任意一个$(T_{i}^{(\exists X)intf}.\text{ }{{M}_{k}})\in {{S}^{M}}, T_{i}^{(\exists X)intf}\in {{S}^{{{T}^{(\exists X)intf}}}};$

(3)    S^entry⊆S^M表示开始节点集合;

(4)    S^terminate⊆S^M表示终止节点集合;

(5)    R表示调用关系集合, 对于任意一个$\langle T_{i}^{(\exists X)intf}.\text{ }{{M}_{k}}, T_{j}^{(\exists X)intf}.\text{ }{{M}_{l}}\rangle \in R或\langle {{D}_{s}}.\text{ }T_{i}^{(\exists X)intf}, {{D}_{t}}.\text{ }T_{j}^{(\exists X)intf}\rangle \in R$, 表示

$ T_{i}^{(\exists X)intf}\xrightarrow{invocable({{M}_{k}}, {{M}_{l}})}T_{j}^{(\exists X)intf}或{{D}_{s}}\xrightarrow{invocable(T_{i}^{(\exists X)intf}, T_{j}^{(\exists X)intf})}{{D}_{t}}. $

在依据V_ASAMM逐层建模中, 可采用课题组开发的基于形式化方法和DSL^[14]的图形工具进行G_DSI设计, 刻画应用系统体系结构的设计要求, 确定基本接口类型中各个方法之间的可调用关系.

3.3 基于调用图G_DSI的期望性质规约

本文采用V_ASAML描述需求期望性质, 由此使模型和性质规约采用同一种语言.

定义5(类型序列).设T_k(k=1, …, n)是类型, 如果类型T_i和类型T_j(1≤i, j≤n)之间应满足以下某一种类型关系, 则称T₁; …; T_n为一个类型序列.

(1)    类关联关系:${{T}_{i}}\overset{R}{\longleftrightarrow}{{T}_{j}}$.

(2)    对象关联关系:${{T}_{i}}\overset{a\text{ }:\text{ }R}{\longleftrightarrow}{{T}_{j}}$.

(3)    参数关联关系:${{T}_{i}}\xrightarrow{in\text{ }/<<param>>}{{T}_{j}}$或${{T}_{i}}\xrightarrow{out\text{ }/<<param>>}{{T}_{j}}$.

(4)    子类型关联关系:$S\text{:}T\text{, }$其中$S, T\in \left\{ {{T}_{1}}, ..., {{T}_{n}} \right\}$.

(5)    方法关联关系:${{T}_{i}}\xrightarrow{methods}{{T}_{j}}$.

(6)    成员类型关联关系:${{T}_{i}}\xrightarrow{member}{{T}_{j}}$.

(7)    泛化关联关系:$T_{i}^{intf}\xrightarrow{generalize}T_{j}^{(\exists X)intf}.$

(8)    方法可调用关系:${{T}_{i}}\xrightarrow{invocable}{{T}_{j}}$.

(9)    可传参调用关系:${{T}_{i}}\xrightarrow{pass-parameter}{{T}_{j}}$.

(10)    设备类型可连通关系:${{D}_{s}}\overset{linkable}{\longleftrightarrow}{{D}_{t}}$或〈D_s|D_t〉_T, 其中, D_s, D_t, T∈{T₁, …, T_n}.

(11)    设备类型服务可调用关系:${{D}_{s}}\xrightarrow{invocable(T_{i}^{(\exists X)intf}, T_{j}^{(\exists X)intf})}{{D}_{t}}$, 其中, D_s, D_t∈{T₁, …, T_n}.

定义6(类型序列正确性).设{R₁, …, R_k}是如上定义的类型序列T₁; …; T_n对应的类型关系的集合, 则T₁; …; T_n正确当且仅当R₁∧…∧R_k成立.

本文所设计有向图G_DSI可转换为机器可处理的文档(如XML文档), 保持与G_DSI具有相同的语义, 从而使得调用图G_DSI可以反映应用系统体系结构中实际设计要求.在定义5和定义6的基础上, 通过遍历设备类型服务调用图G_DSI, 可自动生成期望性质公式.其基本思想是:采用深度优先遍历方式, 查找由开始节点到所有终止节点之间的可达路径, 并由该路径上所有节点上的类型产生类型序列, 由它们之间的关系产生相应的类型关系集合.其算法伪代码如下所示.

算法4. GenerateProperties(·).

Input: G_DSI转换文本.

1.    list←null; path←null; typeseq←null; //$list\text{=}\varnothing \text{ }|\text{ }\cup {{\{{{T}_{1}};...;{{T}_{m}}\}}_{\{{{R}_{1}}, \ldots , {{R}_{k}}\}}}$, 1≤m, 0≤k

2.    path←getUnvisitedPath(G); //深度优先查找所有可达路径中未被访问路径

3.    if path≠null then

4.      for each node in pathTmp

5.        typeseq=typeseq.add(path.node[i].type);

6.      end for

7.      for each arc in path

8.        relationset=relationset.add(path.arc[i].relation)

9.      end for

10.  end if

11.  if (typeseq≠null) then

12.      list.add(typeseq, relationset)

13.  end if

Output:list.

上述算法输出应用系统体系结构模型期望性质, 即类型序列及其关系集合.对应连通性需求和互操作性两方面的部署需求.因此本文在验证部也分为连通性验证、互操作验证两部分, 其中, 互操作性又包括设备类型服务可调用和求值验证两部分.连通性验证和服务可调用验证部分利用类型序列及其关系集合描述所期望的性质, 通过V_ASAML语言的类型检查算法检查模型中是否定义了期望的类型及类型规则; 在求值验证方面, 基于V_ASAML语言中定义的求值规则, 根据调用图G_DSI上一组给定的实参, 验证其每一条可达路径上相邻的方法$T_{i}^{intf}.\text{ }{{M}_{k}}$的λ项进行求值, 并验证是否与期望结果相同.

3.4 V_ASAMS原型系统

V_ASAMS系统基于本文V_ASAML语言、V_ASAMM方法及其类型检查算法开发提供建模和验证环境, 其总体构成如图 2所示, 分为3个部分, 支持需求导入、系统建模和性质验证.

●   需求导入是对应用系统部署需求进行分析, 形成应用系统体系结构规划, 由此产生设备类型服务调用图G_DSI作为实际设计要求导入V_ASAMS, 并通过遍历该有向图, 可自动生成需求期望的性质公式.

●   系统建模采用本文建模范式, 自底向上构建应用体系结构各层类型及其关系.

●   性质验证对所创建应用体系结构模型连通性和互操作性两部分进行验证.其中,

1)    连通性验证是对连通性期望性质公式里每个逻辑单元中的连通性相关的类型关系能否满足进行判定, 并计算出这一命题是否成立, 若成立, 则表示所创建的应用体系结构模型满足设计要求中的可连通性, 说明具备部署要求中对网络环境相关基本条件.

2)    设备互操作性验证首先对互操作性期望性质公式里每个逻辑单元中的可调用关系能否满足进行判定, 并计算出这一性质的命题是否成立, 若成立, 则表示所创建的应用系统体系结构模型满足设计要求中的可互操作性, 说明具备部署要求中对基础软件环境相关基本条件; 其次, 通过指定类型变量将环境中所有泛化接口类型进行实例化得到接口类型, 并进一步遍历设备类型服务调用图G_DSI中每条可达路径上的接口类型, 生成接口对象及其λ表达式, 通过给定实参进行λ求值, 并将结果与期望的值进行比较, 若与期望值相同, 说明当前设计要求符合部署需求.若验证通过, 则表示该应用系统体系结构模型可以作为设计, 指导部署和系统运维.

V_ASAMS可自动推理应用系统体系结构设计的正确性.其工作原理是, 首先对应用系统体系结构设计要求导入并解析和自动生成需求期望性质公式; 其次自底向上对应用系统体系结构进行设计, 支持基本组成部分的检索和查询; 最后自动验证应用系统体系结构基本组成部分的连通性和互操作性.

采用J2EE应用系统开发框架结合函数式编程语言OCaml-Java^[31]和开源数据库实现了V_ASAMS.该系统可通过网页版用户接口面向需求分析方、部署设计方、设计验证方等用户提供服务.需求分析方可管理和维护设备类型及其功能, 可对导入的G_DSI进行解析; 部署设计方可自底向上分层构建应用系统体系结构模型; 设计验证方将需求期望性质自动生成后, 可以触发系统自动判定所建应用系统体系结构是否满足需求期望性质.

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

本文应用系统体系结构建模和验证案例包括需求分析、建模和验证这3个部分.本案例的需求为设计某行业应用系统运行环境, 并验证该运行环境满足应用系统部署的实际要求, 即设计应用系统体系结构并验证需求满足性.该应用系统体系结构由网络设施、硬件设备、基础软件和应用软件及其相关配置组成.其中, 网络设施、硬件设备应根据行业实际需求采购, 并根据应用系统体系结构要求进行实施和配置, 基础软件和应用软件则根据应用系统体系结构要求进行安装或部署.

4.1 某行业应用系统体系结构需求分析

本案例应用系统体系结构中应用软件部分的整体组成如图 3所示, 包括4个组成部分, 它们分别通过政务网和互联网提供服务.其中, 政务网中包括为行业各层机构提供的政务业务服务和为行业相关管理机构提供的行业管理服务, 而互联网部分包括为社会公众提供的行业公共服务和政务公共服务.这4个组成部分合起来为行业服务保障体系和行业服务监管体系的建立和协同提供了信息化支撑.

4.1.1 应用系统体系结构原始需求

上述应用软件通常是基于互联网技术的Web应用软件.将其合理部署于数据中心机房, 形成相应的应用系统之后方可对外提供服务.本案例中, 应用系统体系结构需求见表 2.其中, 第2列为原始需求, 第3列为依据Web应用软件满足需求采取的常规方法^[20]给出的需求分析.

由表 2可以引申出, 应用系统体系结构从构成要素上包括网络设备、防火墙、路由器以及应用服务器、数据库服务器、文件服务器和存储服务器等各类服务器硬件设备, 同时还包括操作系统、应用中间件、数据库管理软件等基础软件以及部署或运行于其上的应用软件.本案例应用系统中, 应用软件的访问用户又分为互联网用户、省级VPN用户和运维VPN用户这3类, 表 2中的需求3~需求6限定了该行业应用系统不同类型的访问用户应有不同的访问路径, 即根据图 3中行业应用软件的4个组成部分, 不同类型的访问用户经由一系列必要的网络设备(如数据中心防火墙、DMZ以及核心路由器等)到达应用系统区域后, 根据其访问应用软件的不同, 使其访问路径不同, 具体需求见表 3.

表 3给出了应用系统体系结构中, 每条访问路径上不同设备之间的互操作的原始需求.

4.1.2 应用系统体系结构设计要求

设计要求作为应用系统体系结构建模的依据, 也是一个形式化模型, 本文采用定义4设备类型服务调用图刻画.为了得到这一模型作为建模的实际设计要求, 首先将需求分析内容以部署规划图的形式展现, 再根据部署规划图生成设备类型服务调用图G_DSI.根据表 2和表 3中的需求和常规Web应用系统体系结构设计^{[20, 32]}, 以图形化方式展现了案例中某行业应用系统的构成部署规划图如图 4所示, 它包括核心交换区、DMZ区、运维管理区、服务计算区、数据库服务区以及存储区等6个部分.其行业应用软件的部署区域为图 4中左下部分的服务计算区, 根据图 3应用软件构成, 该区又可细分为业务交换服务区、业务系统区、计算服务区和渲染服务区等众多区域.此外, 为了达到服务质量的要求^[33], 在规划中对上述划分的区域应进行IP地址划分, 形成不同网段后, 应引入集群或负载均衡配置.

图 4中, 设备名称、类型及各区网段已在图中标识, 设备之间的连线如图 5所示的6种图例, 包括心跳线、软件集群、设备集群以及各类网络连接线.图 4和图 5是构造设备类型服务调用图的基础.

此外, 图 4还展现了表 3中该应用系统的访问用户的5条访问路径, 根据所划分的网段, 可通过防火墙策略配置将不同角色用户的访问路径相互隔离.其具体规划见表 4.

上述部署规划中, 涉及不同类型的软硬件设备及其功能.对本案例相关软硬件设备的功能从硬件网络接口、防火墙、交换机和操作系统以及其他基础软件等几个维度进行分类, 对它们进行统一编码, 并对它们所提供的主要功能加以整理^[34-36], 则可由部署规划图得到设备类型服务调用图G_DSI, 作为本案例应用系统体系结构的设计要求, 如图 6所示.

图 6是一个有向图, 其中每个节点标记为“设备类型编号!功能类型编号.功能₁, 功能₂, …”的形式, 每一条边标记为“功能类型编号.功能₁; 功能₂; …”的形式, 分别表示访问路径上每个相关设备以及跳转至下一个节点所要触发的功能.例如, 节点Dev5!Tintf9.M25, M26, M27, M28表示设备Dev5通过功能类型Tintf9的功能M25, M26, M27可到达Dev6!Tintf11.M36, M37, M38, M39节点.

可将图 6转化为相同语义的XML文件, 并将该XML文件录入V_ASAMS系统进行解析, 可给出具体的设计要求, 如下定义所示.

${{G}_{DSI}}=\{{{S}^{{{T}^{intf}}}}, {{S}^{M}}, {{S}^{entry}}, {{S}^{terminate}}, R\}$包括:

(1)    ${{S}^{{{T}^{intf}}}}=\{T_{i}^{intf}|T_{i}^{intf}(1\le i\le 25)\}$为应定义的接口类型, 共25个.

(2)    ${{S}^{M}}=\{(T_{i}^{intf}.\text{ }{{M}_{k}})|T_{i}^{intf}\in {{S}^{{{T}^{intf}}}}, {{M}_{k}}\in \Gamma \}$为应定义的接口类型方法, 共70个.

(3)    ${{S}^{entry}}=\{T_{j}^{intf}|T_{j}^{intf}(j=1, 2, 3, 21)\}\subseteq {{S}^{M}}$为数据中心防火墙接口类型及其方法构成的顶点, 应定义16个接口类型及其有限多个方法.

(4)    ${{S}^{terminate}}=\{T_{k}^{intf}|T_{k}^{intf}(k=1, 2, 3, 16, 20)\}\subseteq {{S}^{M}}$为存储或审计接口类型及其方法构成的顶点, 应定义25个接口类型及其有限多个方法.

(5)    $R=\left\{ T_{i}^{intf}\xrightarrow{invokable({{M}_{k}}, {{M}_{l}})}T_{j}^{intf}, {{D}_{s}}\xrightarrow{invokable(T_{i}^{intf}, T_{j}^{intf})}{{D}_{t}} \right\}\text{, }1\le i, j\le 25, 1\le k, l\le 70, 1\le s, t\le 11$为接口类

型方法之间的调用关系和设备类型服务调用关系集合, 应定义至少43个接口类型方法调用关系和23个设备类型服务调用关系.

设备类型服务调用图为应用系统体系结构各层的建模和验证提供了依据.将相关设备的每一条基本功能对应到带标签的映射类型, 将每个功能类型对应到基本接口类型, 将一组功能类型对应到相应的软硬件设备, 则可逐层构建应用系统体系结构.在验证部分, 可由设备类型服务调用图自动生成可达路径上的类型序列及其关系作为模型所需满足的性质公式, 并利用V_ASAMS系统进行验证.下面根据图 6逐层进行应用系统体系结构建模.

4.2 某行业应用系统体系结构建模

应用系统体系结构集软硬件于一体, 涉及多种硬件和基础软件.软硬件通过对外提供接口(API)实现各种功能.不同的接口聚合成为不同的软硬件设备.随着软件定义的网络的发展, 软件定义的硬件设备得到进一步的发展^[37], 说明可从软件的角度视察硬件.就硬件设备而言, 从其电子线路接口到用户操作接口等众多接口都属于API(应用程序接口), 本文重点考虑其中影响部署中的可连通性与互操作性等主要性质的接口, 并采用带标签的映射类型进行刻画.类似地, 就基础软件而言, 从其软件代码接口到系统服务接口等众多接口也都属于API, 本文仍着重考虑其中对系统部署具有重要意义的接口, 并采用带标签的映射类型进行刻画.应用软件形成应用系统包括3个基本过程:(1)将相关硬件设备连接; (2)在硬件设备上安装基础软件并进行相关配置; (3)在相关基础软件中部署应用软件并进行相关配置.参考这一过程, 为刻画应用系统体系结构中的软硬件设备, 首先从功能中抽象出一组基本数据类型和API接口(即带标签的映射类型), 其次为该功能构造基本接口类型^[11], 之后根据基本接口类型构造软硬件设备类型.鉴于一个应用软件可运行环境的多样性, 在构造基本接口类型时引入存在量词, 构造泛化接口类型, 使得带标签的映射类型中包含类型变量.当一个泛化接口类型中所有的类型变量都替换为某个具体的类型后, 称作接口类型.本文应用系统体系结构所涉及的硬件设备或基础软件的功能, 从抽象的角度看, 或者是接口类型, 或者是泛化接口类型(即带存在量词接口类型).

为满足需求, 首先将需求分析内容转化为应用系统体系结构的实际设计要求, 然后采用图 2中的V_ASAMS系统, 利用V_ASAML语言和V_ASAMM方法对某行业应用体系结构进行建模, 包括M_bd(基本数据类型), M_bti(基本接口类型), M_dev(设备类型)和M_frwk(应用系统框架)建模等4个建模过程.

4.2.1 基本数据类型

对应用系统体系结构进行建模, 首先根据设备类型服务调用图定义基本数据类型.基本数据类型建模是构造基本接口类型的基础.基本数据类型由数据类型、扩展数据类型和标签映射类型这3个部分组成.根据该应用系统相关软硬件, 本文设计了IPAddress、Context、URI、UserAgent、cookie、ConfigFile、Script、ServerName、FWPolicy等上百种数据类型, 分别编号为B₀~B₁₂₇, 以及将它们通过“乘”“和”“幂”“加标签”或“映射”等操作构造而成数十种扩展数据类型, 分别编号为BE₁~BE₇₁, 见表 5.此外, 该层还包括数十种带标签的映射类型, 是对相关软硬件设备的功能抽象出的一组接口, 分别编号为M₁到M₉₁.它们是将数据类型或扩展数据类型再通过通过“乘”“和” “幂”“加标签”或“映射”等操作构造而成的类型, 见表 6.数据类型、扩展数据类型和带标签的映射类型合起来构成应用系统体系结构模型中基本数据类型M_bd层, 其类型总数为290个.表 5给出了基本数据类型的定义方式, 表 6给出了带标签的映射类型的定义方式.

由表 5的数据类型和扩展数据类型及表 6的带标签映射类型合起来构成了基本数据类型.每一个基本数据类型由一般常见的数据类型或领域中已定义的数据类型通过“乘”“和”“幂”“加标签”或“映射”等操作构造而成^[9], 本案例所有基本数据类型构成M_bd层的类型部分, 该层的类型关系以聚合关系和参数关联关系为主, 分别为91和202个.其中, 层内基本数据类型之间的参数关联关系个数为24个, 它们与带标签的映射类型之间的输入参数关联关系和输出参数关联关系分别为88和90个.本文假定文中所定义的M_bd层数据类型均可由给定环境直接识别, 这一前提也是本文类型检查的基础.

4.2.2 基本接口类型建模

在M_bd层的基础上, 可对基本接口类型进行建模.

本文对基本接口类型定义为形如{[∃X]^*, {[l:X]^*, [l:T₁]^*, [l:T₂]^*, methods:{[l:T₁→T₂]^*}}}的类型项.构建基本接口类型时, 根据图 6设备类型服务调用图的设计要求, 将每个节点对应到某个软硬件设备的某个功能名称, 它们的方法(methods)对应一组带标签的映射类型.映射类型类型表达式左端(输入参数)和右端(输出参数)是基本数据类型.根据设计要求解析, 本案例应包括表 7所示26个基本接口类型.

由于基本接口类型是对设备功能的抽象, 每个功能又由一组API实现, 因此上述每一个基本接口类型的方法部分源于M_bd层中的一组带标签映射类型.其中, 有些接口类型用于设备之间的连接, 有些接口类型用于设备之间的互操作.由于应用系统体系结构是面向运行环境中对应用软件的部署过程, 因此在抽象过程中主要面向部署, 不考虑和部署无关的部分.并且由于应用系统体系结构存在多样性, 可在建模中使用存在量词修饰类型变量, 抽象软硬件设备的功能.因此, 下面针对应用系统体系结构中与部署相关的两个重要性质, 连通性和互操作性等方面, 对相关基本接口类型的建模给出详细说明.

●   连通性相关接口类型

设备可以通过硬件网络接口中的以太网服务组成LAN网, 根据协议的不同, 以太网服务包括基于IP和基于光纤通道两类, 实现数据链路层的帧封装和帧重构, 如公式(1)和公式(2)所示.

$ \left. \begin{align} & T_{1}^{intf}=IPNWService \\ & IPNWService=\{\exists IPPacket, \exists Frame \\ & \text{ }\{ippack:IPPacket, mac:MACAddress, frame:Frame, \\ & \text{ }methods:\{ \\ & \text{ }DataEncapsulate:IPPacket\times MACAddress\to Frame, \\ & \text{ }RebuildData:Frame\times MACAddress\to IPPacket\}\}\} \\ \end{align} \right\} $

(1)

$ \left. \begin{align} & T_{26}^{intf}=FCoEService \\ & FCoEService=\{\exists IPPacket, \exists Frame \\ & \text{ }\{ippack:IPPacket, mac:MACAddress, frame:Frame, \\ & \text{ }methods:\{ \\ & \text{ }DataEncapsulate:IPPacket\to Frame\times MACAddress, \\ & \text{ }\operatorname{Re}buildData:Frame\times MACAddress\to IPPacket\}\}\} \\ \end{align} \right\} $

(2)

其中, $T_{1}^{intf}$和$T_{26}^{intf}$分别为接口类型IPNWService和FCoEService.设备之间能够互连互通除了上述硬件网络接口之外, 还需要操作系统实现网络层协议, 并通过其用户操作接口中的网络通信类管理命令提供基本的检查和配置功能, 如公式(3)和公式(4)所示(其中, $T_{2}^{intf}和T_{3}^{intf}$分别为接口类型ETHService和UserInterfaceService).

$ \left. \begin{align} & T_{2}^{intf}=ETHService \\ & ETH=\{\exists TCPPacket, \exists IPPacket, \exists Data \\ & \text{ }\{data:Data, ippack:IPPacket, b:Boolean, localaddr:LocalAddress, \\ & \text{ }pr:PingResult, hn:HoseName, tcppacket:TCPPacket, tr:TransResult, \\ & \text{ }methods:\{ \\ & \text{ }encapsulate:Data\times HostName\times Port\to TCPPacket, \\ & \text{ }decapsulate:TCPPacket\to Data\times HostName\times Port, \\ & \text{ }ipencapsulate:TCPPacket\to IPPacket, \\ & \text{ }ipdecapsulate:IPPacket\to TCPPacket, \\ & \text{ }TransData:((LocalAddress\to Ping\operatorname{Re}sult)\times Data\times HostName\times Port)\to TransResult, \\ & \text{ }RecieveData:((IPPacket\to TCPPacket))\to Data\times HostName\times Port)\}\}\} \\ \end{align} \right\} $

(3)

$ \left. \begin{align} & T_{3}^{intf}=UserInterfaceService \\ & UserInterfaceService=\{\exists TCPPacket, \\ & \text{ }\{intf:InterfaceId, ipaddr:IPAddress, b:Boolean, pr:PingResult, \\ & \text{ }methods:\{ \\ & \text{ }upcmd:InterfaceId\to IPAddres{{s}^{*}}, \\ & \text{ }downcmd:\{InterfaceId+IPAddress\}\to Boolean, \\ & \text{ }pingcmd:IPAddress\to PingResult, \\ & \text{ }remoteConncmd:IPAddress\to Boolean, \\ & \text{ }excutecmd:File\to Boolean\}\}\} \\ \end{align} \right\} $

(4)

设备也可以通过硬件网络接口中的存储局域网服务组成存储局域网(SAN), 根据协议的不同, SAN服务包括基于FC-SANService和基于iSCSI-SANService两类, 实现网络连接和数据转发^[38].如公式(5)和公式(6)所示, 定义$T_{15}^{intf}和T_{16}^{intf}$两个接口类型如下:

$ \left. \begin{align} & T_{15}^{intf}=FC\_SANService \\ & FC\text{-}SANService=\{\exists FCData, \exists DataBlock, \\ & \text{ }\{fcd:FCData, dbl:DataBlock, \\ & \text{ }methods:\{ \\ & \text{ }ForwardDataBlock:DataBlock\times FCPortN{{o}^{*}}\to FCData, \\ & \text{ }RecieveDataBlock:FCData\to DataBlock\times FCPortN{{o}^{*}}\}\}\} \\ \end{align} \right\} $

(5)

$ \left. \begin{align} & T_{16}^{intf}=iSCSI\_SANService \\ & iSCSI\text{-}SANService=\{\exists Data, \exists SCSICmd, \\ & \text{ }\{data:Data, scsicmd:SCSICmd, \\ & \text{ }methods:\{ \\ & \text{ }ForwardDataBlock:Data\times HostName\times Port\times SCSICmd\to TCPPacket, \\ & \text{ }RecieveDataBlock:TCPPacket\to Data\times HostName\times Port\times SCSICmd\}\}\} \\ \end{align} \right\} $

(6)

上述定义中:公式(1)、公式(2)、公式(5)、公式(6)由硬件驱动实现, 它们是局域网内设备连接和存储局域网内设备连接的基础, 属于硬件网络的接口类型; 公式(3)和公式(4)由操作系统实现, 属于基础软件的接口类型.

●   互操作性相关接口类型

根据需求中每一类设备的功能类型列表, 本文还给出了基础软件的其他接口类型^[34-36], 它们是设备之间实现互操作的必要条件.以基础软件中间件为例, 包括几个典型的接口类型:HTTP协议处理模块、应用服务器管理模块和应用处理模块, 它们的定义如公式(7)~公式(9)所示.

$ \left. \begin{align} & T_{9}^{intf}=HTTPProtocolHandler \\ & HTTPProtocolHandler=\{\text{ }\exists Context, \exists StaticResource, \exists DynamicResource, \\ & \text{ }\exists StaticFile, \exists CallRequest, \exists ProcessResult, \\ & \text{ }\{req:HTTPRequest, ctx:Context, sr:StaticResource, \\ & \text{ }dr:DynamicResource, sf:StaticFile, cr:CallRequest, pr:ProcessResult, \\ & \text{ }rcr:RemoteCallRequest, ra:RemoteAddress, res:HTTPResponse, \\ & \text{ }methods:\{ \\ & \text{ }RecieveReq:HTTPRequest\to Context, \\ & \text{ }ProcessReq:((Context\to (StaticResource+DynamicResource))\to \\ & \text{ }(StaticFile+CallRequest))\to ProcessResult, \\ & \text{ }RemoteReq:CallRequest\to (RemoteCallRequest\times RemoteAddress), \\ & \text{ }ResponseReq:ProcessResult\to HTTPResponse\}\}\} \\ \end{align} \right\} $

(7)

$ \left. \begin{align} & T_{10}^{intf}=ASServerManager \\ & ASServerManager=\{\text{ } \\ & \text{ }script:Script, laddr:ListenAddress, b:Boolean, \\ & \text{ }cf:ConfigFile, dp:DeploymentPlan, \\ & \text{ }methods:\{ \\ & \text{ }StartupServer:ConfigFile\times \{StartupScript:Script\}\to ListenAddress, \\ & \text{ }ShutdownServer:ConfigFile\times \{ShutdownScript:Script\}\to Boolean, \\ & \text{ }DeployApp:ConfigFile\times DeploymentPlan\times \{DeployScript:Script\}\to ConfigFile, \\ & \text{ }ConfigRS:ConfigFile\to ConfigFile, \\ & \text{ }StartupService:ConfigFile\times \{StartupSvcScript:Script\}\to Boolean, \\ & \text{ }StopService:ConfigFile\times \{StopSvcScript:Script\}\to Boolean, \\ & \text{ }UndeployApp:ConfigFile\times DeploymentPlan\times \{UnDeployScript:Script\}\to ConfigFile\}\} \\ \end{align} \right\} $

(8)

$ \left. \begin{align} & T_{11}^{intf}=APPHandler \\ & APPHandler=\{\exists RemoteCallRequest, \exists Object, \exists Method, \exists CallRequest, \exists ProcessResult, \\ & \text{ }\{rcreq:RemoteCallRequest, o:Object, m:Method, sql:SQLStatement, dbn:DBName \\ & \text{ }cr:CallRequest, pr:ProcessResult, para:Parameters \\ & \text{ }methods:\{ \\ & \text{ }RecieveCall:(RemoteCallRequest\times ListenAddress)\to (Object\times Method\times Parameters) \\ & \text{ }ProcessCall:((Object\times Method\times Parameters)\to NoError)\to CallRequest, \\ & \text{ }DACallRequest:((Object\times Method\times Parameters)\to (Account\times DBName\times SQLStatement)) \\ & \text{ }ReturnCallResult:(DBData+CallRequest)\to ProcessResult\}\}\} \\ \end{align} \right\} $

(9)

上述3个基本接口类型中, 公式(7)和公式(9)属于泛化接口类型, 若将它们的类型变量指定为某个类型, 即被实例化后, 将具有实际含义.例如, 公式(9)接口类型APPHandler中有一个远程调用类型变量RemoteCallRequest, 在具体的应用服务器中, 该类型变量可能被实例化为EJB中的Skeleton Object的方法调用, 也可能被实例化为CORBA中的Remote Application Object的方法调用或DCOM中的Remote Process Call的方法调用, 从而反映实际远程调用的方式^[39].

应用系统体系结构中, 有些接口类型的构成是更为复杂的高阶类型, 即映射类型的两端可以是映射类型.例如, 公式(7)中接口类型HTTPProtocolHandler中的方法ProcessReq是一个高阶的接口类型, 如下定义所示.

ProcessReq:((Context→(StaticResource+DynamicResource))→(StaticFile+CallRequest))→ProcessResult.

HTTP请求的处理过程为:根据HTTP请求解析获得的上下文Context, 判断该请求为静态或是动态资源请求.如果为静态资源请求, 则根据静态文件生成处理结果(本地处理); 如果是动态资源请求, 则继续通过远程调用请求后端应用服务器进行进一步处理, 并根据远程调用的结果生成最终处理结果ProcessResult.其中, 判断静态与否以及判断本地处理或远程调用部分又是一种接口, 因此, 该接口类型可以称为泛化接口类型.接口类型HTTPProtocolHandler用于刻画Web服务器的HTTP请求处理功能.本案例涉及26个接口类型的详细定义, 它们构成M_bti层的类型部分, 该层的类型关系以方法关联关系和成员关联关系为主, 分别为93和167个.类型关系对应的类型规则可自动生成, 如BE₁ in/param M1和B₇₃ out/param M1对应的参数关联关系的类型规则如公式(10)和公式(11)所示, 方法关联和成员关联关系的类型规则如公式(12)和公式(13)所示.

$ \left. \begin{align} & B{{E}_{1}}\xrightarrow{in/\langle \langle param\rangle \rangle }{{M}_{1}}或 \\ & IPPacket\times MACAddress\xrightarrow{in/\langle \langle param\rangle \rangle }DataEncapsulate:MACAddress\times IPPacket\to Frame \\ \end{align} \right\} $

(10)

$ {{B}_{73}}\xrightarrow{out/\langle \langle param\rangle \rangle }{{M}_{1}}或Frame\xrightarrow{out/\langle \langle param\rangle \rangle }DataEncapsulate:MACAddress\times IPPacket\to Frame $

(11)

$ {{M}_{1}}\xrightarrow{methods}T_{1}^{intf}或DataEncapsulate:MACAddress\times IPPacket\to Frame\xrightarrow{methods}IPNWService $

(12)

$ \left. \begin{align} & {{B}_{71}}\xrightarrow{member}T_{1}^{intf}, {{B}_{72}}\xrightarrow{member}T_{1}^{intf}, {{B}_{73}}\xrightarrow{member}T_{1}^{intf}或\\ & MACAddress\xrightarrow{member}IPNWService, IPPacket\xrightarrow{member}IPNWService, Frame\xrightarrow{member}IPNWService \\ \end{align} \right\} $

(13)

上述每个基本接口类型对应于设计要求中某个设备的一个功能名称, 每个功能名称对应一组功能方法, 因此在基本接口类型建模过程中, 系统会提示当前接口类型还需聚合哪些功能方法, 即带标签的映射类型.所聚合的带标签的映射类型与该接口类型之间的方法关联关系对应的类型规则由V_ASAMS系统自动生成.接口类型是构造设备类型的基础.本案例所定义的接口类型可由TCA算法判定, 接口类型之间的关系可由RCA算法判定.

4.2.3 设备类型和应用系统体系结构框架类型建模

设备类型是由基本接口类型聚合而成的类型, 根据图 6设备类型调用图, 本案例涉及的设备类型共11个, 每个设备类型由一组基本接口类型聚合的乘积类型, 其定义见表 8.

表 8中, 第3列为设备类型的类型表达式, 它们构成M_dev层的类型部分.该层的类型关系以层内类型关联关系和层间聚合关系为主, 分别为125和52个.类型关系对应的类型规则可自动生成.

上述每个设备类型对应于设计要求中的某个设备, 若某个设备的建模中没有聚合足够多的基本接口类型, 则因缺少对应的聚合类型关系, 而使得该设备相关的验证不能通过.每个设备类型所聚合的基本接口类型与该设备类型之间聚合关系对应的类型规则由V_ASAMS系统自动生成.设备是构造应用系统体系结构类型的基础.本案例所定义的设备可由TCA算法判定, 设备类型之间的关系可由RCA算法判定.

根据图 6设备类型服务调用图, 本案例应用系统体系结构框架类型为1个, 涉及11种类型的设备, 定义如下:

$ AF{{W}_{1}}=\left\{ \begin{matrix} \{De{{v}_{2}}\times , ..., \times De{{v}_{12}}\} \\ {{R}_{ij}}(AF{{W}_{1}}, De{{v}_{i}}), j=1, 2\le i\le 12 \\ \end{matrix} \right\}. $

其中, R_ij为该层层内及层间类型关系.容易看出, 其中的聚合关系数为11个.根据任意类型是自身的子类型, 整个应用系统体系结构类型中的子类型关系个数和基本数据类型中不同类型间的子类型关系数分别为329和26.

应用系统体系结构类型对应于完整的设计要求, 若在建模中没有聚合足够多的设备类型, 则因缺少对应的聚合类型关系, 而使得该设备相关的验证不能通过.每个应用系统体系结构类型所聚合的设备类型与该应用系统体系结构类型之间聚合关系对应的类型规则由V_ASAMS系统自动生成.

4.2.4 接口类型λ表达式

本案例中的设备类型型号版本以及IP规划和环境变量设置可作为实参用于本案例基本接口类型的实例化过程, 并最终可得到接口对象列表.它们是模拟设备类型之间通过接口类型实际互操作的基础.

4.3 某行业应用系统体系结构验证

本节首先给出某行业应用系统体系结构模型需要验证的性质, 并采用V_ASAMS原型系统对所创建模型进行验证.为此, 首先根据设备类型服务调用图利用GenerateProperties算法生成应用系统体系结构模型所期望的性质公式P; 其次, 利用类型序列正确性检查算法(CheckCorectness)判定P中的每一组设备类型序列是否正确, 从而验证P是否成立.

表 9中给出了部署规划中的5条访问路径, 每条路径上的设备类型序列以及相邻设备之间的关系构成每条路径上的性质, 将它们分别记为P₁~P₅.

每条路径上涉及两类的关系:一是连通性, 二是互操作性.连通性包括以太网连通和存储局域网连通, 互操作性是指相连设备之间可调用关系的集合以及实际互操作性模拟结果的集合.为了后续验证方便, 假设Elink= (IPNWService+FCoEService)表示或者实现以太网或者实现光纤以太网接口的类型, Slink=(FC_SANService+ iSCSI_SANService)表示或者实现光纤存储局域网或者实现iSCSI存储局域网接口的类型, 则根据定义3, 两个设备类型D₁和D₂可通过以太网连通, 当且仅当Elink < :D₁, Elink < :D₂, 记为${{D}_{1}}\overset{E-linkable}{\longleftrightarrow}{{D}_{2}}$或〈D₁|D₂〉_Elink; 类似地, 两个设备类型D₁和D₂可存储局域网连通, 当且仅当Slink < :D₁, Slink < :D₂, 记为${{D}_{1}}\overset{S-linkable}{\longleftrightarrow}{{D}_{2}}$或〈D₁|D₂〉_Slink.路径上相邻设备两个设备类型D₁和D₂可互操作, 当且仅当它们之间存在可调用关系, 即${{D}_{1}}\xrightarrow{invocable(T_{i}^{intf}, T_{j}^{intf})}{{D}_{2}}$.路径上相邻设备两个设备类型D₁和D₂实际可互操作, 当且仅当该路径上某个系统级操作根据已知的参数(如IP地址)和输入参数(如目标IP地址或目标路径), 通过λ演算模拟执行, 验证能否得到期望的值.

采用V_ASAMS系统可以得到上述5个路径上的连通性和互操作性相关的性质公式, 其定义见表 9, 给出了5个访问路径上的设备类型序列及其关系集合.其中$R_{se{{q}_{i}}}^{link}和R_{se{{q}_{i}}}^{coop}$(1≤i≤9)分别表示设备连通性和互操作性相关的关系集合.

因此, 本案例中应用系统体系结构连通性相关性质$P_{i}^{link}$(1≤i≤5)的公式如下:

$ P_{1}^{link}=R_{se{{q}_{1}}}^{link}\wedge R_{se{{q}_{2}}}^{link}, \text{ }P_{2}^{link}=R_{se{{q}_{3}}}^{link}, \text{ }P_{3}^{link}=R_{se{{q}_{4}}}^{link}, \text{ }P_{4}^{link}=R_{se{{q}_{5}}}^{link}, \text{ }P_{5}^{link}=R_{se{{q}_{6}}}^{link}\wedge R_{se{{q}_{7}}}^{link}\wedge R_{se{{q}_{8}}}^{link}\wedge R_{se{{q}_{9}}}^{link}\text{.} $

而对于设备基本接口类型之间的互操作性, 表 9给出了从数据中心外到内的访问路径上的关系集合, 而对于从数据中心内到外返回路径上的关系集合, 可以采用反向映射的方式标记, 即若$R={{D}_{1}}\xrightarrow{invocable}{{D}_{2}}$, 则${{R}^{-1}}={{D}_{2}}\xrightarrow{invocable}{{D}_{1}}$.类似地, 关系集合R^-1表示对关系集合R中的每一个关系反向映射后的关系的集合.因此, 每条访问路径上的可互操作性$P_{i}^{coop}$(1≤i≤5)的公式如下:

$ \begin{matrix} P_{1}^{coop}=R_{se{{q}_{1}}}^{coop}\wedge R_{se{{q}_{2}}}^{coop}\wedge {{(R_{se{{q}_{1}}}^{coop})}^{-1}}\wedge {{(R_{se{{q}_{2}}}^{coop})}^{-1}}, \text{ }P_{2}^{coop}=R_{se{{q}_{3}}}^{coop}\wedge {{(R_{se{{q}_{3}}}^{coop})}^{-1}}, \\ P_{3}^{coop}=R_{se{{q}_{4}}}^{coop}\wedge {{(R_{se{{q}_{4}}}^{coop})}^{-1}}, \text{ }P_{4}^{coop}=R_{se{{q}_{5}}}^{coop}\wedge {{(R_{se{{q}_{5}}}^{coop})}^{-1}}, \text{ }P_{5}^{coop}=R_{se{{q}_{6}}}^{coop}\wedge R_{se{{q}_{7}}}^{coop}\wedge R_{se{{q}_{8}}}^{coop}\wedge R_{se{{q}_{9}}}^{coop}. \\ \end{matrix} $

结合上述公式, 记${{P}_{i}}=P_{i}^{link}\wedge P_{i}^{coop}$(1≤i≤5), 则某行业应用系统体系结构模型的性质为P=P₁∧P₂∧P₃∧P₄∧P₅.上述P_i(1≤i≤5)所对应的设备类型序列及其关系集合作为需求期望性质公式, 可由V_ASAMS自动生成.

而在验证中, V_ASAMS系统利用CheckCorrectness算法判定每个P_i是否成立, 并计算出P=P₁∧P₂∧P₃∧P₄∧P₅是否成立.若有一项不符合, 则应用系统体系结构建模过程存在错误, 即不能满足需求.以互操作性验证为例, 若发现某些节点类型之间应有关系不存在, 则认为模型不符合设计要求, 从而判定不满足需求, 如图 7所示.

此外, 通过λ演算模拟接口对象的执行, 可验证设备类型之间的实际互操作性的结果.

在V_ASAMS系统中, 设计方可以根据设备类型服务调用图的要求, 反复验证所有可达路径上的连通性和互操作性, 并根据提示修改模型后, 使之最终满足要求.本案例对某行业应用系统体系结构的验证结果如图 8所示.

本案例中经过多次迭代, 连通性性质和互操作性性质验证通过的类型关系个数与其待验证类型关系总数相同, 说明本文设计的应用系统体系结构模型能够满足当前某行业应用系统面向实际部署的需求.

5 结论及未来的工作

本文的主要贡献如下.

1)    提出了一种基于高阶类型理论模型驱动的可验证应用系统体系结构建模语言V_ASAML、建模方法V_ASAMM, 开发了建模验证原型系统V_ASAMS, 包括可验证应用系统体系结构设计的建模编辑环境, 应用系统体系结构需求可满足的验证环境.

2)    提出了基于有向图应用系统体系结构设计要求, 通过扩展定义类型序列正确性, 验证应用系统体系结构模型中的设备连通性和互操作性能否得到满足; 并采用V_ASAML语言设计了某行业应用系统体系结构, 验证了该设计关于需求的可满足性, 关于方法有效性, 基于本文方法实施的应用系统运行环境通过了信息系统安全等保三级.

3)    进一步扩展了作者所在课题组提出的基于类型理论的建模验证方法应用规模, 为建立统一的、采用同一种形式化工具可验证应用系统体系结构建模体系奠定了基础.

本文在已有工作基础上扩展的类型系统是更加复杂的高阶类型系统, 通过引入存在类型(∃X)扩展了语言的描述能力和抽象层次, 未来的工作包括:1)探索在什么条件下可以证明扩展后类型系统中类型检查的可计算性; 2)研究因环境变更驱动和攻/防模型变更驱动的应用系统体系结安全性验证问题.