Tools for Scows

COWS is a calculus strongly inspired by WS-BPEL which combines primitives of well-known process calculi (like, e.g., the pi-calculus) with constructs meant to model web services orchestration.

Two tools, named respectively Scows_amc and Scows_lts, have been developed at UNITN within the EU SENSORIA Project to foster probabilistic model checking of services specified in Scows, a stochastic variant of COWS.

Scows_amc is a tool for the approximate model checking of Scows services The tool, based on the generation of direct simulatons of terms of the language, allows statistical model checking while maintaining acceptable computation time and approximation values. Scows terms can be checked against the usual CSL time-bounded until properties and against numerical time-bounded until formulae.
A description of Scows_amc can be found in Approximate Model Checking of Stochastic COWS.

Scows_lts allows exact model checking of Scows terms against CSL properties. This is achieved by providing a suitable interface to PRISM: the Labelled Transition System associated to the stochastic specification is first derived, then its corresponding Continuous Time Markov Chain is generated and recorded in the same notation adopted by PRISM.
A description of Scows_lts can be found in A Tool for Checking Probabilistic Properties of COWS Services.