PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
De Nicola R., Latella D., Massink M. Formal modeling and quantitative analysis of KLAIM-based mobile systems. FULL VERSION. The document has been submitted to Conference: 20th ACM Symposium on Applied Computing (SAC 2005) - Track on Coordination Models, Languages and Applications, Technical report, 2004.
 
 
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, like most web-based service implementations. In this paper we propose STOcKLAIM, a STOchastic extension of cKLAIM the core subset of KLAIM. cKLAIM includes process distribution, process mobility, and asynchronous communication. The extension makes it possible to integrate the modeling of quantitative aspects of mobile systems---e.g. performance---with the functional specification of such systems. At the conceptual level, our proposal is based on the assumption that any action of a process in a cKLAIM network takes some time to be executed. At the technical level, the time associated to the execution of an action is determined by a continuous random variable with an exponential distribution. Consequently, process actions in STOcKLAIM are equipped with the rate of such distributions. We present a formal operational semantics of STOcKLAIM which associates a labeled transition system to each STOcKLAIM network and a translation from such labeled transition systems to Continuous Time Markov Chains for quantitative analysis. We also show how STOcKLAIM can be used by means of two simple examples: namely a distributed mobile service and the spreading of a virus.
Subject Formal Modeling and Validation
Stochastic Behaviour
Mobile Systems
Coordination Languages
D.2.4 Software/Program Verification: Formal Methods
68Q10 Modes of computation (nondeterministic, parallel, interactive,probabilistic, etc.)
68Q55 Semantics
68Q85 Models and methods for concurrent and distributed computing(process algebras, bisimulation, transition nets, etc.)


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