MoSL: A Stochastic Logic for StoKLAIM

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. This paper concentrates on their integration with performance and dependability aspects, the logical characterization of performance and dependability requirements, and the automatic validation of system models against integrated formal functional and performance/dependability requirements. To that purpose the temporal logic MoSL is introduced for formulating properties of models specified in StoKLAIM, a Markovian extension of KLAIM introduced in previous work of the authors. MoSL is inspired by (an action-based version of) CSL, an extension of CTL with ample means to refer to performance and dependability aspects. It is shown that a substantial fragment of the logic can be mapped onto the input language of existing probabilistic model checkers, thus allowing for the automated verification of qualitative and quantitative properties of network-aware programs. The approach is illustrated by modeling and verifying the spreading of a virus through a network.