Klaim is an experimental language designed for modeling and programming distributed systems composed of mobile components where distribution awareness and dynamic system architecture configuration are key issues. StocKlaim [13] is a Markovian extension of the core subset of Klaim which includes process distribution, process mobility, asynchronous communication, and site creation. In this paper, MoSL, a temporal logic for StocKlaim is proposed which addresses and integrates the issues of distribution awareness and mobility and those concerning stochastic behaviour of systems. The satisfiability relation is formally defined over labelled Markov chains. A large fragment of the proposed logic can be translated to action-based CSL for which efficient model-checkers exist. This way, such model-checkers can be used for the verification of StocKlaim models against MoSL properties. An example application is provided in the present paper.
Towards a logic for performance and mobility
Latella D.;Massink M.
2006
Abstract
Klaim is an experimental language designed for modeling and programming distributed systems composed of mobile components where distribution awareness and dynamic system architecture configuration are key issues. StocKlaim [13] is a Markovian extension of the core subset of Klaim which includes process distribution, process mobility, asynchronous communication, and site creation. In this paper, MoSL, a temporal logic for StocKlaim is proposed which addresses and integrates the issues of distribution awareness and mobility and those concerning stochastic behaviour of systems. The satisfiability relation is formally defined over labelled Markov chains. A large fragment of the proposed logic can be translated to action-based CSL for which efficient model-checkers exist. This way, such model-checkers can be used for the verification of StocKlaim models against MoSL properties. An example application is provided in the present paper.File | Dimensione | Formato | |
---|---|---|---|
prod_176533-doc_6279.pdf
accesso aperto
Descrizione: QAPL2005
Tipologia:
Versione Editoriale (PDF)
Licenza:
Creative commons
Dimensione
355.68 kB
Formato
Adobe PDF
|
355.68 kB | Adobe PDF | Visualizza/Apri |
2005_a3_27.pdf
accesso aperto
Descrizione: Towards a Logic for Performance and Mobility
Tipologia:
Documento in Pre-print
Licenza:
Nessuna licenza dichiarata (non attribuibile a prodotti successivi al 2023)
Dimensione
268.45 kB
Formato
Adobe PDF
|
268.45 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.