Web服务组合隐私需求的时序属性分析与验证研究

摘要

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

目录

封面

声明

中文摘要

英文摘要

目录

图表清单

缩略词

第一章 绪论

1.1 课题研究背景及意义

1.2 研究现状及选题依据

1.3 论文组织结构

第二章 基于模型检验的Web服务组合隐私保护

2.1 Web服务隐私保护

2.2 模型检验方法

2.3 基于模型检验的Web服务组合隐私需求验证框架

2.4 本章小结

第三章 隐私需求时序属性分析及规约

3.1 隐私需求中数据依赖关系分析

3.2 隐私需求时序属性对Web服务行为的约束

3.3 隐私需求的线性时序逻辑规约

3.4 本章小结

第四章 WS-BPEL隐私行为建模

4.1 隐私接口自动机

4.2 WS-BPEL的隐私接口自动机建模

4.3 隐私接口自动机到Promela模型的转换

4.4 本章小结

第五章 隐私需求验证原型工具的设计与实现

5.1 隐私需求验证系统设计

5.2 工具实现

5.3 应用实例分析

5.4 本章小结

第六章 总结与展望

6.1 论文工作总结

6.2 进一步工作

参考文献

致谢

在学期间的研究成果及发表的学术论文