Quantitative Analysis of Services

We show a number of applications of the tools which have been developed within the sensoria project to perform quantitative analysis of services. These tools are formally grounded on source calculi which allow the description of services at distinct levels of abstraction, and hence pose distinct challenges to both modelling and analysis. The reported applications refer to (suitable subcomponents of) the Finance Case-Study, and show instances of, respectively, exact model checking of MarCaSPiS against the both state-aware and action-aware logic SoSL, exact and statistical model checking of sCOWS against the state-aware logic CSL, querying of PEPA models by terms of the XSP language that expresses both state-aware and action-aware stochastic probes.