Istituto di Scienza e Tecnologie dell'Informazione     
De Nicola R., Latella D., Massink M. Formal modeling and quantitative analysis of KLAIM-based mobile systems. In: Annual ACM Symposium on Applied Computing (SAC'2005) (Santa Fe, New Mexico, USA, March 13 -17, 2005). Proceedings, pp. pages 428 - 435. H. Haddad, L. Liebrock, A. Omicini, R. Wainwright, M. Palakal, M (eds.). Association for Computing Machinery, 2005.
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. 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. We present a formal operational semantics of STOcKLAIM, which associates a labeled transition system to each STOcKLAIM network and a translation to Continuous Time Markov Chains for quantitative analysis. We also show how STOcKLAIM can be used by means of a simple example, i.e. the modeling of the spreading of a virus.
Subject Formal Modeling and Validation
Stochastic Behavior
Mobile Systems
Coordination Languages
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