D4.1.a Stochastic Core Calculi

This deliverable reports on the quantitative extensions of formalisms related to the core calculus under investigation in WP2. In particular, it addresses three main quantitative extensions that have been developed so far: stochastic extension of KLAIM, stochastic extension of beta-binders and a probabilistic extension of a Linda-like language for SOC.

D4.1.b Stochastic Reasoning on Core Calculi

This deliverable reports on stochastic extensions of calculi for service oriented computing developed until M36 by the SENSORIA Project partners involved in WP4. Reflecting the evolution in the calculi developed within WP2, reported by deliverables D2.1.a and D.TH01.a, the stochastic calculi presented in this deliverable are more mature with respect to the ones developed in the early stages of WP4 and are able to deal with mechanisms typical of the service oriented paradigm. Moreover, such calculi constitute a linguistic framework in which the results of deliverable D.TH03.a, concerning quantitative and qualitative measurements of quality of service and service level agreements, can be applied.

D4.2.a Stochastic Logics

The present deliverable addresses the complementary issue of integrated formal characterisation of functional, performance, and dependability measures and requirements on (STOKLAIM) models for global computing. In particular it focuses on a logical characterisation of relevant functional properties and performance/dependability measures. To that purpose the Mobile Continuous Stochastic Logic (MOSL) is proposed which, basically, is a temporal logic that permits describing the dynamic evolution of the system, both action- and state-based, a real-time logic that permits the use of real-time bounds in the logical characterisation of the behaviours of interest and a probabilistic logic that permits expressing not only functional properties, but also properties related to performance and dependability aspects, and, finally, a spatial logic that addresses the spatial structure of the network for the specification.

D4.2.b Model Checking Stochastic Logics

Deliverable D4.2.a addressed the complementary issue of integrated formal characterisation of functional, performance, and dependability measures and requirements on models for global computing specified by STOKLAIM. In particular it focused on a logical characterisation of relevant functional properties and performance/dependability measures by means of the Mobile Continuous Stochastic Logic (MOSL). This is a temporal logic that permits describing the dynamic evolution of the system and that permits the use of real-time bounds in the logical characterisation of the behaviours of interest. Indeed, MOSL is a probabilistic logic that permits expressing not only functional properties, but also properties related to performance and dependability aspects.
In this deliverable we present MOSL+; an extension of MOSL, which incorporates some basic features of the Modal Logic for MObility (MOMO), a logic specifically designed for dealing with resource management and mobility aspects of concurrent behaviours. We also show how MOSL+ formulae can be model-checked against STOKLAIM specifications. To this purpose we show how existing state-based stochastic model-checkers, like e.g. the Markov Reward Model Checker (MRMC), can be exploited by
using a front-end for STOKLAIM that performs appropriate pre-processing of MOSL+ formulae.

D4.3.a Quantitive Mesaurements of Quality of Service for Service Level Agreements

Quantitative analysis of quality-of-service metrics is an important tool in early evaluation of service provision. This analysis depends on being able to estimate the average duration of critical activities used by the service but at the earliest stages of service planning it may be impossible to obtain accurate estimates of the expected duration of these activities. The time-dependent behaviour of an automotive rescue service in the context of uncertainty about durations is analyzed and a distributed computing platform to allow the efficient derivation of quantitative analysis results across the range of possible values for assignments of durations to the symbolic rates of our high-level formal model of the service expressed in a stochastic process algebra is deployed.

D4.4.a Quantitytive Techniques for Measuring Resource Usage

When specifying the expected resource usage of programs, it will usually turn out that the actual resource behavior of certain operations (actions) of the program depends not only on the data input into those operations, but also on how this data interacts with other data in the program. This is especially true for memory usage-perhaps the most important of resources.

For this reason, we have decided that when developing methods for measuring quantitative resource usage, one should first develop methods for describing how objects share resources. In the case of memory, this means considering how objects are layed out in memory.

In the proposed approach, the layout of objects in memory is described using algebraic, coalgebraic and behavioural specification methods. Using algebraic methods is justified by their standard character and by the existence of properly formalised algebraic specification languages. The use of coalgebraic and behavioural notions, on the other hand, turns out to perfectlymatch the needs of providing a sufficiently abstract specification method for resources.

D4.4.b Quantitative Techniques for Measuring Resource Usage (second version)

We refine here our proposed methodology for specification and verification of memory usage as presented in Deliverable D4.4a to arbitrary abstract resources. It turns out the the necessary adjustments are rather direct, and the ideas, concepts and results concerning the memory usage carry over to this more general setting. The approach is presented in an informal manner; although some definitions are given precisely, the presentation is guided by examples, and formal statements of relevant theorems and technical facts are avoided.

D4.a: Quantitative Reasoning on the Financial Case Study

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 actionaware 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 actionaware stochastic probes.