SENSORIA - D4.2a - Stochastic logics

The programming and modeling language KLAIM has been designed to address key functional aspects of global computing such as distribution awareness, (code and agent) mobility, and privacy aspects. A stochastic extension of KLAIM, StoKLAIM has been proposed in Sensoria Deliverable D4.1a for the integrated formal modeling of the above mentioned aspects of global computing with performance and dependability ones. 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) a temporal logic that permits describing the dynamic evolution of the system; (b) both action-}and state-based, (c) a real-time logic that permits the use of real-time bounds in the logical characterisation of the behaviours of interest, (d) a probabilistic logic that permits expressing not only functional properties, but also properties related to performance and dependability aspects; and, finally, (e) a spatial logic that addresses the spatial structure of the network for the specification. The presentation of MoSL provided in the present report is rather informal and given mainly by means of a simple but representative running example, which is used also for illustrating how stochastic model checking can be used for automatic analysis of qualitative as well as quantitative aspects of models. The general issue of the logical characterisation of performance/dependability related properties is addressed by means of examples as well; in particular we use the Airbag Scenario} of the Sensoria Automotive Case Study.