Quantitative Analysis of Mobile and Distribute Systems: The KLAIM Approach.


Dott. Michele Loreti.


Aula 2 Collegio Raffaello (Piazza della Repubblica 13).


17:00 - 19:00.

Numero di crediti:


Vincoli di partecipazione:



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.

Docente di riferimento:

Prof. Marco Bernardo.

Ultima modifica: 03/05/2007 Approvato da: Presidente CCdL