發(fā)布時(shí)間：2018-05-17 12:06

  本文選題：Web服務(wù)組合 + 隱私需求　； 參考：《南京航空航天大學(xué)》2014年碩士論文

【摘要】：隨著面向服務(wù)架構(gòu)SOA（Service-oriented Architecture）的發(fā)展，Web服務(wù)組合已經(jīng)應(yīng)用到日常生活的各個(gè)領(lǐng)域。用戶在使用Web服務(wù)組合時(shí)，需要提供一些個(gè)人隱私信息以完成必要的業(yè)務(wù)功能。所以，在滿足業(yè)務(wù)需求的前提下，，保護(hù)用戶隱私安全已經(jīng)成為當(dāng)前服務(wù)計(jì)算領(lǐng)域的研究熱點(diǎn)。隱私保護(hù)本質(zhì)是隱私需求的滿足，Web服務(wù)環(huán)境的動(dòng)態(tài)、異構(gòu)和自治的特征，使得隱私保護(hù)必須考慮服務(wù)間的行為交互，必須對(duì)用戶隱私數(shù)據(jù)以及它們之間的依賴關(guān)系加以限制。由于一些隱私數(shù)據(jù)依賴關(guān)系可以表達(dá)成時(shí)序?qū)傩约s束，考慮到在計(jì)算機(jī)領(lǐng)域模型檢驗(yàn)技術(shù)能夠?qū)Υ?yàn)證系統(tǒng)中時(shí)序相關(guān)特性進(jìn)行精確地驗(yàn)證，本文提出一種基于模型檢驗(yàn)的方法來分析與驗(yàn)證Web服務(wù)組合隱私需求的時(shí)序?qū)傩�。采用線性時(shí)序邏輯規(guī)約隱私需求中隱私數(shù)據(jù)時(shí)序依賴關(guān)系，針對(duì)隱私屬性對(duì)WS-BPEL服務(wù)組合流程抽象建模，并利用模型檢驗(yàn)工具進(jìn)行隱私需求形式化驗(yàn)證。本文的主要研究?jī)?nèi)容如下： （1）分析隱私需求中隱私數(shù)據(jù)時(shí)序依賴關(guān)系與Web服務(wù)行為約束之間的對(duì)應(yīng)關(guān)系，提出一種用線性時(shí)序邏輯規(guī)約隱私需求的方法，并從隱私需求的時(shí)序?qū)傩灾刑崛〕鲵?yàn)證性質(zhì)。 （2）對(duì)接口自動(dòng)機(jī)進(jìn)行隱私屬性擴(kuò)展，得到隱私接口自動(dòng)機(jī)，利用該模型對(duì)Web服務(wù)組合的隱私行為進(jìn)行建模，并給出BPEL流程活動(dòng)到隱私接口自動(dòng)機(jī)的轉(zhuǎn)換方法。然后提出轉(zhuǎn)換算法將該模型轉(zhuǎn)換成模型檢驗(yàn)工具SPIN能夠接收的Promela描述。 （3）基于本文的研究方法，設(shè)計(jì)并實(shí)現(xiàn)了Web服務(wù)組合隱私需求驗(yàn)證原型工具，利用該工具對(duì)WS-BPEL流程進(jìn)行隱私行為建模，并借助SPIN完成隱私需求的時(shí)序?qū)傩则?yàn)證。最后通過一個(gè)實(shí)例說明本文方法的可行性和有效性。
[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.
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2014
【分類號(hào)】：TP393.09

【參考文獻(xiàn)】

相關(guān)期刊論文 前4條

1 周航;黃志球;祝義;夏良;劉林源;;基于Time Petri Net的實(shí)時(shí)系統(tǒng)沖撞檢測(cè)與消解[J];計(jì)算機(jī)研究與發(fā)展;2012年02期

2 趙亮;黃志球;劉林源;;Web服務(wù)組裝中的隱私暴露分析方法[J];計(jì)算機(jī)科學(xué)與探索;2012年04期

3 賈哲;黃志球;王珊珊;沈國(guó)華;柯昌博;;支持本體推理的P3P隱私策略沖突檢測(cè)研究[J];計(jì)算機(jī)科學(xué)與探索;2013年01期

4 岳昆,王曉玲,周傲英;Web服務(wù)核心支撐技術(shù):研究綜述[J];軟件學(xué)報(bào);2004年03期

相關(guān)博士學(xué)位論文 前1條

1 劉林源;Web服務(wù)組合隱私分析與驗(yàn)證研究[D];南京航空航天大學(xué);2011年

本文編號(hào)：1901296