TY - CHAP
T1 - Model checking single web services using Markov Chains and MDPs
AU - Oghabi, Giti
AU - Bentahar, Jamal
AU - Benharref, Abdelghani
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
KW - Model Checking
KW - Verification
KW - Web Service
UR - http://www.scopus.com/inward/record.url?scp=80052705006&partnerID=8YFLogxK
U2 - 10.3233/978-1-60750-831-1-20
DO - 10.3233/978-1-60750-831-1-20
M3 - Chapter
AN - SCOPUS:80052705006
SN - 9781607508304
T3 - Frontiers in Artificial Intelligence and Applications
SP - 20
EP - 37
BT - New Trends in Software Methodologies, Tools and Techniques Proceedings of the Tenth SoMeT_11
ER -