Model checking single web services using Markov Chains and MDPs

Giti Oghabi, Jamal Bentahar, Abdelghani Benharref

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


This paper proposes a new verification method for individual web service specified using OWL-S, the Ontology Web Language for semantic web Services, where probabilities are introduced to model uncertain choices. The approach makes use of a probabilistic model checker named PRISM. The web service description is received as an input in form of OWL-S, which is analyzed and automatically transformed into a Discrete Time Markov Chain (DTMC) or a Markov Decision Process (MDP). The obtained DTMC/MDP is then 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. In addition to the atomic processes, different composite processes are considered including sequence, choice, if-then-else, repeat-while, repeat-until, split, and split join. We also prove that the transformation algorithm is sound and complete and introduce a software tool implementing the approach.

Original languageBritish English
Title of host publicationNew Trends in Software Methodologies, Tools and Techniques Proceedings of the Tenth SoMeT_11
Number of pages18
StatePublished - 2011

Publication series

NameFrontiers in Artificial Intelligence and Applications
ISSN (Print)0922-6389


  • Model Checking
  • Verification
  • Web Service


Dive into the research topics of 'Model checking single web services using Markov Chains and MDPs'. Together they form a unique fingerprint.

Cite this