● 摘要
作为云计算三种主要的服务模式之一，软件即服务(Software as a Service, SaaS)越来越受到普遍关注。在多租户SaaS环境中，租户通过租用和组合组件构建SaaS应用程序，极大地降低了使用成本。但是，由于租户租用的组件可能来自于不同的提供商，因此这些应用程序的可靠性无法得到保证。而传统情况所采用的软件测试方案也存在测试用例缺失，耗时过长以及无法在组合前进行测试等不足。与软件测试不同，软件验证可以在组件组合前证明组合的可靠性。然而，现有的验证方案却无法满足多租户SaaS环境的需求。
首先，多租户SaaS环境中组件数量庞大，且组件间拥有众多的组合可能性。针对本文这个问题，本文提出了一套基于MTA的验证即服务(Verification as a Service, VaaS)方案，设计了其体系结构和服务流程。该方案包含组件建模，模型转换，分布式组合验证等核心服务。
其次，研究了组件建模的方法，通过实例分析，选用Bigraph对组件进行描述。针对Bigraph没有成熟模型检验工具的问题，本文形式化地给出了Bigraph模型中节点、端口、边、反应规则到PROMELA的转换方法，并实现了模型转换工具Bigraph2PROMELA。同时，在定义验证服务的基础上，结合MapReduce框架和SPIN工具，将验证服务分布到不同的验证节点执行，并通过组合的方式得到验证结果，显著提高了验证服务的执行效率。
最后，通过实例验证了VaaS方案的可行性，并设计不同的样例进行对比实验，分析了分布式组合验证服务的执行效率。