云计算服务通常是在一个动态、开放的网络环境下进行的。云计算服务固有的动态性和不稳定性导致服务的失效频发,给构建云计算可信服务带来了新的挑战。本文的目标是研究如何构建云计算环境中的可信服务系统,从云计算可信服务模型的构建着手,提出了该模型的Petri网形式化描述方式。结合面向方面的编程思想,将云计算服务中的可信性质抽象为可信方面网,描述云计算服务的可信服务行为；针对云计算服务的安全访问、故障检测及测试用例生成等提高云计算服务可信性的行为进行形式化建模,并利用模型检验技术和典型样例实验对云计算服务的可信行为属性进行了验证,实验结果表明该方法的可行性和有效性。本文的主要工作和创新性包括以下几个方面。1.面向方面的云计算可信服务建模研究对研究涉及的面向方面编程及Petri网理论进行了研究。结合面向方面及层次着色Petri网理论,提出了云计算可信服务形式化一般描述模型(CTN)。给出了CTN构建的流程及其模型的Petri网形式化描述。为后续的三个提高云计算服务可信性的具体措施的形式化建模及分析提供理论基础。通过将云计算可信服务中的可信性需求从业务流程中分离出来,形成可信横切关注点,进而利用层次着色Petri网形式化描述该横切关注点的可信属性和行为特征,建立云计算可信服务Petri网模型。经过关注点的抽取及层次化处理,降低了模型分析的复杂度,提高了建模效率。而精确的Petri网形式化描述及推理验证,有效增强了应用模型构建的实际云计算服务系统的可信性。2.云计算可信服务的安全访问控制策略研究(1)从云计算可信服务访问需求出发,基于AOP及CTN模型,研究云计算可信服务的访问控制方面网的构造,用精确的语言表述用户对云计算可信服务的安全需求。(2)根据云计算服务执行流程,利用描述语言从云计算环境中的托管应用系统的行为角度构建云计算服务的访问控制模型。(3)基于模型的执行语义,综合考虑云计算可信服务的的服务质量,研究云计算可信服务的访问控制策略。综合利用面向方面编程思想,研究可扩展的云计算可信服务的访问控制实施方案,并给出模型验证方法,以保障系统稳定运行,从而解决云计算环境中访问机制的动态实施问题。(4)提出了适合云计算环境的安全访问模型和实施方法,可解决云计算环境的资源虚拟化、边界动态、应用托管等特征给安全带来的难题。3.云计算可信服务故障检测方法研究以云计算可信服务的业务流程为核心,应用CTN模型开展云计算可信服务的拜占庭故障诊断的形式化建模与分析研究工作。利用CTN模型构建了云计算可信服务系统的故障诊断模型,包括计算资源、网络资源的描述,任务之间数据和逻辑关系、任务与资源之间的匹配关系、故障类型和特征等。根据故障类型和特征,提出了部分节点轮换检测策略,并利用CTN模型刻画检测策略的实施,同时借助Petri网的操作语义及模型状态空间验证提出的云计算可信服务故障检测方法的正确性和有效性,并进一步给出检测的实现算法。4.云计算可信服务测试方法研究针对云计算可信服务测试的特点,基于CTN模型分别对云计算环境下可信服务的不同组件进行建模。基于面向方面思想编织云计算可信服务的核心关注点和测试关注点(包括组件测试关注点和服务组合测试关注点),并利用编织机制将这些模块动态地集成为一个完整的云计算可信服务测试模型。在此基础上,本文提出了云计算可信服务的测试用例选择策略,将其抽象成一个横切关注点织入到云计算可信服务的测试模型中,并给出测试用例选择的实施算法,同时借助Petri网的操作语义及状态空间分析云计算可信服务测试的正确性及有效性。