论文部分内容阅读
随着面向服务架构SOA（Service-oriented Architecture）的发展，Web服务组合已经应用到日常生活的各个领域。用户在使用Web服务组合时，需要提供一些个人隐私信息以完成必要的业务功能。所以，在满足业务需求的前提下，保护用户隐私安全已经成为当前服务计算领域的研究热点。隐私保护本质是隐私需求的满足，Web服务环境的动态、异构和自治的特征，使得隐私保护必须考虑服务间的行为交互，必须对用户隐私数据以及它们之间的依赖关系加以限制。由于一些隐私数据依赖关系可以表达成时序属性约束，考虑到在计算机领域模型检验技术能够对待验证系统中时序相关特性进行精确地验证，本文提出一种基于模型检验的方法来分析与验证Web服务组合隐私需求的时序属性。采用线性时序逻辑规约隐私需求中隐私数据时序依赖关系，针对隐私属性对WS-BPEL服务组合流程抽象建模，并利用模型检验工具进行隐私需求形式化验证。本文的主要研究内容如下：（1）分析隐私需求中隐私数据时序依赖关系与Web服务行为约束之间的对应关系，提出一种用线性时序逻辑规约隐私需求的方法，并从隐私需求的时序属性中提取出验证性质。（2）对接口自动机进行隐私属性扩展，得到隐私接口自动机，利用该模型对Web服务组合的隐私行为进行建模，并给出BPEL流程活动到隐私接口自动机的转换方法。然后提出转换算法将该模型转换成模型检验工具SPIN能够接收的Promela描述。（3）基于本文的研究方法，设计并实现了Web服务组合隐私需求验证原型工具，利用该工具对WS-BPEL流程进行隐私行为建模，并借助SPIN完成隐私需求的时序属性验证。最后通过一个实例说明本文方法的可行性和有效性。