Formal modeling and quantitative analysis of KLAIM-based mobile systems

KLAIM is an experimental language designed for modeling and programming distributed systems composed of mobile components where distribution awareness and dynamic system architecture con- figuration are key issues. In this paper we propose STOcKLAIM, a STOchastic extension of cKLAIM, the core subset of KLAIM. cKLAIM includes process distribution, process mobility, and asyn- chronous communication. The extension makes it possible to in- tegrate the modeling of quantitative aspects of mobile systems-- e.g. performance--with the functional specification of such sys- tems. We present a formal operational semantics of STOcKLAIM, which associates a labeled transition system to each STOcKLAIM network and a translation to Continuous Time Markov Chains for quantitative analysis. We also show how STOcKLAIM can be used by means of a simple example, i.e. the modeling of the spreading of a virus