Towards a logic for performance and mobility

Rocco De Nicola, Joost P. Katoen, Diego Latella, Mieke Massink

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

8 Citations (Scopus)

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 [R. De Nicola, D. Latella, and M. Massink. Formal modeling and quantitative analysis of KLAIM-based mobile systems. In ACM Symposium on Applied Computing (SAC). ACM Press, 2005. Also available as Technical Report 2004-TR-25; CNR/ISTI, 2004] 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.
Original languageUndefined
Title of host publication3rd Workshop on Quantitative Aspects of Programming Languages
EditorsA. Cerone, H. Wiklicky
Place of PublicationAmsterdam
PublisherElsevier
Pages161-175
Number of pages15
DOIs
Publication statusPublished - 2006

Publication series

NameElectronic Notes in Theoretical Computer Science
PublisherElsevier
Number2
Volume153
ISSN (Print)1571-0661
ISSN (Electronic)1571-0661

Keywords

  • IR-54800
  • METIS-229289
  • EWI-8235

Cite this

De Nicola, R., Katoen, J. P., Latella, D., & Massink, M. (2006). Towards a logic for performance and mobility. In A. Cerone, & H. Wiklicky (Eds.), 3rd Workshop on Quantitative Aspects of Programming Languages (pp. 161-175). (Electronic Notes in Theoretical Computer Science; Vol. 153, No. 2). Amsterdam: Elsevier. https://doi.org/10.1016/j.entcs.2005.10.037
De Nicola, Rocco ; Katoen, Joost P. ; Latella, Diego ; Massink, Mieke. / Towards a logic for performance and mobility. 3rd Workshop on Quantitative Aspects of Programming Languages. editor / A. Cerone ; H. Wiklicky. Amsterdam : Elsevier, 2006. pp. 161-175 (Electronic Notes in Theoretical Computer Science; 2).
@inproceedings{828002b64209431b82e03075154b07ae,
title = "Towards a logic for performance and mobility",
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 [R. De Nicola, D. Latella, and M. Massink. Formal modeling and quantitative analysis of KLAIM-based mobile systems. In ACM Symposium on Applied Computing (SAC). ACM Press, 2005. Also available as Technical Report 2004-TR-25; CNR/ISTI, 2004] 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.",
keywords = "IR-54800, METIS-229289, EWI-8235",
author = "{De Nicola}, Rocco and Katoen, {Joost P.} and Diego Latella and Mieke Massink",
note = "Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL 2005), April 2-3, 2005, Edinburgh, UK",
year = "2006",
doi = "10.1016/j.entcs.2005.10.037",
language = "Undefined",
series = "Electronic Notes in Theoretical Computer Science",
publisher = "Elsevier",
number = "2",
pages = "161--175",
editor = "A. Cerone and H. Wiklicky",
booktitle = "3rd Workshop on Quantitative Aspects of Programming Languages",

}

De Nicola, R, Katoen, JP, Latella, D & Massink, M 2006, Towards a logic for performance and mobility. in A Cerone & H Wiklicky (eds), 3rd Workshop on Quantitative Aspects of Programming Languages. Electronic Notes in Theoretical Computer Science, no. 2, vol. 153, Elsevier, Amsterdam, pp. 161-175. https://doi.org/10.1016/j.entcs.2005.10.037

Towards a logic for performance and mobility. / De Nicola, Rocco; Katoen, Joost P.; Latella, Diego; Massink, Mieke.

3rd Workshop on Quantitative Aspects of Programming Languages. ed. / A. Cerone; H. Wiklicky. Amsterdam : Elsevier, 2006. p. 161-175 (Electronic Notes in Theoretical Computer Science; Vol. 153, No. 2).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Towards a logic for performance and mobility

AU - De Nicola, Rocco

AU - Katoen, Joost P.

AU - Latella, Diego

AU - Massink, Mieke

N1 - Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL 2005), April 2-3, 2005, Edinburgh, UK

PY - 2006

Y1 - 2006

N2 - 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 [R. De Nicola, D. Latella, and M. Massink. Formal modeling and quantitative analysis of KLAIM-based mobile systems. In ACM Symposium on Applied Computing (SAC). ACM Press, 2005. Also available as Technical Report 2004-TR-25; CNR/ISTI, 2004] 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.

AB - 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 [R. De Nicola, D. Latella, and M. Massink. Formal modeling and quantitative analysis of KLAIM-based mobile systems. In ACM Symposium on Applied Computing (SAC). ACM Press, 2005. Also available as Technical Report 2004-TR-25; CNR/ISTI, 2004] 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.

KW - IR-54800

KW - METIS-229289

KW - EWI-8235

U2 - 10.1016/j.entcs.2005.10.037

DO - 10.1016/j.entcs.2005.10.037

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 161

EP - 175

BT - 3rd Workshop on Quantitative Aspects of Programming Languages

A2 - Cerone, A.

A2 - Wiklicky, H.

PB - Elsevier

CY - Amsterdam

ER -

De Nicola R, Katoen JP, Latella D, Massink M. Towards a logic for performance and mobility. In Cerone A, Wiklicky H, editors, 3rd Workshop on Quantitative Aspects of Programming Languages. Amsterdam: Elsevier. 2006. p. 161-175. (Electronic Notes in Theoretical Computer Science; 2). https://doi.org/10.1016/j.entcs.2005.10.037