PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
De Nicola R., Katoen J., Latella D., Massink M. Towards a logic for performance and mobility. Full Version. The document has been submitted to Conference: 3rd Workshop on Quantitative Aspects of Programming Languages - QAPL'05, Technical report, 2005.
 
 
Abstract
(English)
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 is a Markovian extension of the core subset of KLAIM which includes process distribution, process mobility, asynchronous communication, and site creation. By enriching process actions with specific rates characterizing the exponential distributions modelling the durations of such actions, the extension makes it possible to integrate the modelling of quantitative aspects of mobile systems---e.g. performance---with the functional specification of such systems. 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 translation of the logic to action-based CSL is provided which allows to use of existing aCSL model-checkers for the verification of STOcKLAIM models against MoSL properties. Examples of applications are provided as well.
Subject Stochastic Logics
Mobile Systems
Stochastic Process Algebra
F.3 LOGICS AND MEANINGS OF PROGRAMS
G.3 PROBABILITY AND STATISTICS
C.4 PERFORMANCE OF SYSTEMS
68Q60 Specification and verification
68Q85 Models and methods for concurrent and distributed computing


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