MarCaSPiS: a Markovian Extension of a Calculus for Services. MarCaSPiS is the markovian extension of CaSPiS (Calculus of Sessions and Pipelines). CaSPiS is a core calculus where sessions and pipelines are viewed as natural constructorsfor structuring client-service interaction and service orchestration. MarCaSPiS permits an integrated analysis of both qualitative and quantitative aspects of formal specifications of services. To specify quantiative properties of MarCaSPiS specifications logic SoSL (Service Oriented Stochastic Logic) has been introduced. This is a stochastic logic specifically designed for dealing with specific features of Service Oriented Computing. SoSL is a temporal logic that permits describing the dynamic evolution of the system and it is both action- and state-based and it is equipped with primitives that permit the use of real-time bounds in the logical characterisation of the behaviours of interest. Moreover, SoSL is a probabilistic logic that permits expressing not only functional properties, but also properties related to performance and dependability aspects. Finally, SoSL is a resource oriented logic, which permits addressing openendedness of SOC. Indeed, SoSL provides modal operators that can be used for specifying how a system is able to react to an external stimulus. These allow the verification of assumptions on resources and processes in a system at the logical level, i.e. without having to change the model to investigate the effect of each assumption on the system behaviour. We also have developed ways for model-checking SoSL formulae against MarCaSPiS specifications by exploiting an existing state-based stochastic model-checker (Markov Reward Model Checker, MRMC).