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

发布时间：2018-05-17 12:06

本文选题：Web服务组合 + 隐私需求　；参考：《南京航空航天大学》2014年硕士论文

【摘要】：随着面向服务架构SOA（Service-oriented Architecture）的发展，Web服务组合已经应用到日常生活的各个领域。用户在使用Web服务组合时，需要提供一些个人隐私信息以完成必要的业务功能。所以，在满足业务需求的前提下，，保护用户隐私安全已经成为当前服务计算领域的研究热点。隐私保护本质是隐私需求的满足，Web服务环境的动态、异构和自治的特征，使得隐私保护必须考虑服务间的行为交互，必须对用户隐私数据以及它们之间的依赖关系加以限制。由于一些隐私数据依赖关系可以表达成时序属性约束，考虑到在计算机领域模型检验技术能够对待验证系统中时序相关特性进行精确地验证，本文提出一种基于模型检验的方法来分析与验证Web服务组合隐私需求的时序属性。采用线性时序逻辑规约隐私需求中隐私数据时序依赖关系，针对隐私属性对WS-BPEL服务组合流程抽象建模，并利用模型检验工具进行隐私需求形式化验证。本文的主要研究内容如下：（1）分析隐私需求中隐私数据时序依赖关系与Web服务行为约束之间的对应关系，提出一种用线性时序逻辑规约隐私需求的方法，并从隐私需求的时序属性中提取出验证性质。（2）对接口自动机进行隐私属性扩展，得到隐私接口自动机，利用该模型对Web服务组合的隐私行为进行建模，并给出BPEL流程活动到隐私接口自动机的转换方法。然后提出转换算法将该模型转换成模型检验工具SPIN能够接收的Promela描述。（3）基于本文的研究方法，设计并实现了Web服务组合隐私需求验证原型工具，利用该工具对WS-BPEL流程进行隐私行为建模，并借助SPIN完成隐私需求的时序属性验证。最后通过一个实例说明本文方法的可行性和有效性。
[Abstract]:With the development of Service oriented Architecture (SOA(Service-oriented Architecture), web services composition has been applied to every field of daily life. When using Web services composition, users need to provide some personal privacy information to complete the necessary business functions. Therefore, in order to meet the business requirements, the protection of user privacy security has become the current research hotspot in the field of service computing. The nature of privacy protection is the dynamic, heterogeneous and autonomous characteristics of the Web service environment that satisfy the privacy requirements. Privacy protection must consider the interaction between services and restrict the user's privacy data and their dependencies. Because some privacy data dependencies can be expressed as temporal attribute constraints, considering that in the computer domain model checking technology can accurately verify the temporal correlation characteristics in the verification system. This paper proposes a model-based approach to analyze and verify the temporal attributes of Web services composition privacy requirements. In this paper, the temporal dependence of privacy data in privacy requirements is defined by linear temporal logic, and the WS-BPEL service composition process is modeled abstractly according to privacy attributes, and the formal verification of privacy requirements is carried out by using model checking tools. The main contents of this paper are as follows: 1) analyzing the corresponding relationship between the temporal dependence of privacy data and the behavior constraints of Web services, a method of defining privacy requirements with linear temporal logic is proposed, and the verification properties are extracted from the temporal attributes of privacy requirements. Secondly, the privacy attribute of interface automaton is extended, and the privacy interface automaton is obtained. The model is used to model the privacy behavior of Web service composition, and the transformation method from BPEL process activity to privacy interface automaton is given. Then a transformation algorithm is proposed to transform the model into a Promela description that SPIN can receive. 3) based on the research method of this paper, a prototype tool for Web service composition privacy requirement verification is designed and implemented. The tool is used to model the privacy behavior of WS-BPEL process, and SPIN is used to verify the temporal attributes of privacy requirements. Finally, an example is given to illustrate the feasibility and effectiveness of this method.
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP393.09

【参考文献】