Font Size: a A A

Research On Temporal Property Analysis And Verification Of Privacy Requirement In Web Services Composition

Posted on:2015-04-18Degree:MasterType:Thesis
Country:ChinaCandidate:J J LuFull Text:PDF
GTID:2298330422480989Subject:Computer Science and Technology
Abstract/Summary:PDF Full Text Request
With the development of Service-oriented Architecture (SOC), Web services composition has beenapplied in various fields of daily life. When using Web services composition, consumers have tosubmit some personal private information to support the execution of necessary business process.Therefore, how to protect user privacy has recently become a research focus in the field of servicecomputing. The essence of privacy protection is to satisfy the privacy requirement. The dynamic,heterogeneous and autonomous of Web service characteristics require that privacy protection musttake into account the interaction between services. As a result, the privacy requirements must includethe restriction of both privacy data and the dependencies of them. Some dependencies of privacy datacan be expressed by temporal properties, which can be precisely verified by model checkingapproaches. This paper proposes an approach based on model checking to verify the temporalproperties of privacy requirement in Web services composition. It specifies the temporal dependenciesof privacy data with linear temporal logic, models WS-BPEL process for the extracted privacyproperty and implements verification of privacy requirement by existing moder checker. The majorwork is listed as follows.Firstly, through analysing the correspondence between temporal dependencies of privacy data andbehavior restriction of Web services, the method of extracting linear temporal logic specification fromthe temporal properties of privacy requirement is put forward.Secondly, an approach for modeling the privacy behaviors of Web services composition by privacyinterface automata is proposed, including the transformation from BPEL activities to privacy interfaceautomata. Then, the automa are transformed to Promela description so as to be verified by modelchecker SPIN.Finally, a prototype tool is designed and implemented to conduct privacy modeling for WS-BPELand achieve the temporal property verification of privacy requirement by SPIN. The effectiveness ofproposed method is demonstrated through a case study.
Keywords/Search Tags:Web Services Composition, Privacy Requirement, Temporal Property Verification, Linear Temporal Logic, Interface Automata, Model Checking
PDF Full Text Request
Related items