Web服務(wù)組合隱私需求的時(shí)序?qū)傩苑治雠c驗(yàn)證研究.pdf

1、隨著面向服務(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)系

2、加以限制。由于一些隱私數(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)證。本文的主要研究內(nèi)容如下:
　　(1)分析隱私需求中隱私數(shù)據(jù)時(shí)序依賴關(guān)系與 We

3、b服務(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)證原型