Istituto di Scienza e Tecnologie dell'Informazione     
De Nicola R., Katoen J., Latella D., Massink M. Towards a logic for performance and mobility. In: Electronic Notes in Theoretical Computer Science, vol. 153 (2) pp. 161 - 175. Third Workshop on Quantitative Aspects of Programming Languages. QAPL 2005 (Edinburgh, UK, 02-03 April 2005). Proceedings. A. Cerone and H. Wiklicky (eds.). Elsevier, 2006.
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. $sk{}$~cite{DLM05} is a Markovian extension of the core subset of $k{}$ 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 both the issues of distribution awareness and mobility and those concerning stochastic behaviour of systems. The satisfiability relation is formally defined over (states-/transition-)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.
URL: http://dl.acm.org/citation.cfm?id=1706723
DOI: 10.1016/j.entcs.2005.10.037
Subject Mobility
Stochastic logic
Process algebra
D.2.4 Software/Program Verification

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional