Quantitative Analysis of Distributed Systems in Stoklaim: A Tutorial

Network and distributed systems typically consist of a large number of actors that act and interact with each other in a highly dynamic environment. Due to the number of involved actors and their strong dependence on mobility and interac- tion, performance and dependability issues are of utmost importance for this class of systems. To model these systems many specification languages have been proposed in the literature. One of these is KLAIM: an experimental language specifically de- signed to program distributed systems consisting of several mobile components that interact through multiple distributed tuple spaces. A stochastic extension of KLAIM, named STOKLAIM, has been proposed to facilitate the incorporation of random phenomena. Moreover, to address key functional aspects of STOKLAIM systems such as distribution awareness, mobility, and security and their integration with perfor- mance and dependability guarantees, the temporal logic MoSL has been introduced. In this chapter we show how STOKLAIM and MoSL can be used to specify and verify quantitative properties of distributed systems. These analysis will be performed by relying on statistical model-checking. The use of this relatively new technique permits supporting analysis of large scale systems that, due to the state space explosion problem, cannot be treated via the standard model-checking techniques.