|
Global (or network-aware) computing entails large-scale networks of
computers performing tasks in a cooperative and coordinated manner.
Programming and modeling languages such as KLAIM focus on key functional
aspects of global computing such as distribution awareness, (code and
agent) mobility, and privacy aspects.
We present a revised version of the operational semantics definition for
StoKLAIM, a stochastic extension of KLAIM which permits the description
of random phenomena such as spontaneous computer crashes and spurious
network hick ups. The operational semantics of StoKLAIM is based on
continuous-time Markov chains.
A temporal logic, named MoSL (Mobile Stochastic Logic), is proposed for
specifying properties of models specified in StoKLAIM. The logic is
inspired by (an action-based version of) CSL, an extension of CTL with
ample means to refer to performance and dependability aspects.
We show how MoSL formulae can be model-checked against StoKLAIM
specifications. To this purpose we show how existing state-based
stochastic model-checkers, like e.g. the Markov Reward Model Checker
(MRMC), can be exploited by using a front-end for StoKLAIM that performs
appropriate pre-processing of MoSL formulae.
|