VERIFYING WEB SERVICES USING PROBABILISTIC MODEL CHECKING
Giti Oghabi · Spectrum Research Repository (Concordia University) · 2011
Verifying Web Services using Probabilistic Model Checking Giti OghabiIn service computing, soundness and correctness are key concerns of web services technology.Verification is among the methods used for checking the design's correctness against specific desired properties.Verification means checking a web service in terms of general properties such as safety, liveliness, deadlock freedom, etc.It also means checking if the web service satisfies some specific business-logic properties.Verification aims at increasing the trustworthiness of a web service and decreases its failure rate.In this thesis, we propose a model-checking verification approach for individual web services.We use semantic markup for web services (OWL-S), an Ontology Language for Web Services, to describe web services' behaviors.We introduce probabilities as parameters for this language to model uncertain choices.We use PRISM, a probabilistic model checker to verify web services against general and business-logic properties expressed in a propositional probabilistic logic.In this approach, we develop a transformation algorithm for converting the OWL-S to Markov chain diagram and Markov decision process, which are formal probabilistic models that are compatible with PRISM.The obtained diagram is then automatically processed and coded into the PRISM language.This code is parsed and verified by the PRISM model checker to determine which required properties are satisfied by the web service.We implemented this transformation algorithm and these procedures in a software tool.The fulfillment of this work would not have been possible without the support of many people.I would like to express my sincerest gratitude to my supervisor, Dr. Jamal Bentahar for providing me the opportunity to work in his research team as well as for his kind and endless support, invaluable guidance and precious advice.I would like to thank all my dear lab mates for their help, useful suggestions, sharing experience and the friendly environment they provided in the workplace. My warm appreciation goes to