|
Techniques for Quantitative Analysis |
|
|
Quantitative analysis of for example resource usage or quality-of-service metrics is a powerful tool in early evaluation of service provision. The SENSORIA approach offers the following service description mechanisms and tools facilitating such quantitative analysis of SOAs.
- sCOWS - Stochastic COWS permit the description of services whose basic actions are associated with a rate expressing their delay. This makes sCOWS a language suitable for modelling services whose behaviour can be analysed using Markovian techniques.
- sCOWS_LTS - Tool that offers sCOWS probabilistic model checking through the generation of the LTS (Labelled Transition System) corresponding to the specification, and its subsequent translation to a Continuous Time Markov Chain that can be used as input for the PRISM model checker of CSL (Continuous Stochastic Logic) formulas.
- sCOWS_AMC is a tool that implements approximate statistical model checking of sCOWS terms against CSL. This is obtained by generating simulation traces of computations and applying statistical reasoning.
- SRMC - SENSORIA Reference Markovian Calculus - is a stochastic process calculus which captures the inherent uncertainty in service-oriented systems. The language contains linguistic features to differentiate between systems on the basis of the service providers which they have deployed. These service providers do not need to be performance identical and they do not even need to be identical in behaviour. SRMC allows the model to express both kinds of uncertainty and to evaluate this to give performance predictions which are valid whichever configuration of service providers is selected.
 Analysing an SRMC model
The SRMC language is implemented by transformation into the PEPA process calculus. PEPA - Performance Evaluation Process Algebra - is a concise modelling language which offers the unique capability to analyse models of service-oriented systems using both discrete and continuous methods. The advantage which this flexibility brings is that models of very large systems with large numbers of repeated components, as typically found in service-oriented computing, can be efficiently analysed using continuous methods. This makes the language applicable in modelling domains where other languages fail. In the SENSORIA project we have used the PEPA language to analyse the scalability of large-scale systems.
The PEPA language was enhanced during the SENSORIA project to use an entirely novel continuous-space semantics allowing large-scale models to be solved with ease. The implementation technology for this is a component of the SENSORIA Development Environment, a state-of-theart Eclipse-based tool for formal analysis of service-oriented systems. - MarCaSPiS is a process language specifically designed for addressing quantitative aspects of service-oriented computing. The language is a Markovian extension of the CaSPiS SENSORIA core calculus, the basic concepts being service-definitions, with weighted input activities, service invocations, concretion, and value return, with rated output activities, and sessions.
- SoSL - Service-oriented Stochastc Logic - is a probabilistic, timed, temporal logic, which extends CSL in several ways: it is both state- and action-based and, in particular, classes of actions can be specified by means of action specifiers; moreover, the logic is resource-oriented in order to address open-endedness of service-oriented computing. A stochastic model-checking algorithm and related tool have been developed which use model-checking capabilities of MRMC for checking MarCaSPiS properties expressed in SoSL.
- SoSL-MC is a model checker that permits verifying whether a given MarCaSPiS specification satisfies or not a SoSL formula. The idea is to use an existing state-based stochastic model-checkers, the Markov Reward Model Checker (MRMC), and wrapping them in the SoSL modelchecking algorithm. SoSL-MC, which is implemented in OCaML, permits analysing the execution of MarCaSPiS programs and generating their reachability graphs. Moreover, after loading a MarCaSPiS specification and a formula, it verifies, by means of one or more calls to MRMC, the satisfaction of the formula by the specification.
|
