Towards a logic for performance and mobility. FULL VERSION

KLAIM is an experimental language designed for modeling and programming distributed systems composed of mobile components where distribution awareness and dynamic system architecture configuration are key issues. STOcKLAIM is a Markovian extension of the core subset of KLAIM which includes process distribution, process mobility, asynchronous communication, and site creation. By enriching process actions with specific rates characterizing the exponential distributions modelling the durations of such actions, the extension makes it possible to integrate the modelling of quantitative aspects of mobile systems---e.g. performance---with the functional specification of such systems. In this paper, MoSL, a temporal logic for STOcKLAIM is proposed which addresses and integrates both the issues of distribution awareness and mobility and those concerning stochastic behaviour of systems. The satisfiability relation is formally defined over (states-/transition-)labelled Markov Chains. A translation of the logic to action-based CSL is provided which allows to use of existing aCSL model-checkers for the verification of STOcKLAIM models against MoSL properties. Examples of applications are provided as well.