A Tool for Checking Probabilistic Properties of COWS Services

Abstract. We present a tool developed for fostering probabilistic model checking of services formally specified in Scows, a stochastic enrichment of the Calculus for Orchestration of Web Services. The tool, called Scows lts, derives the Labelled Transition System associated to the term, and further generates the corresponding Continuous Time Markov Chain in the same notation adopted by the PRISM model checker. Scows lts is first described and then seen at work against a small, yet representative, application scenario.

• Type: Journal
• Year: 2010
• Where: TGC
• Authors: Igor Cappello, Paola Quaglia
• Keywords: Applied Computing, Continuous Time Markov Chain, Scows, Scows Lts, TGC 2010