Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., De Nicola R., Loreti M., Massink M. Quantitative analysis of distributed systems in stoklaim: a tutorial. Dario Bruneo, Salvatore Distefano (eds.). Hoboken, NJ, USA: John Wiley & Sons, Inc., 2015.
Network and distributed systems typically consist of a large number of actors that act and interact with each other in a highly dynamic environment. Due to the number of involved actors and their strong dependence on mobility and interaction, performance and dependability issues are of utmost importance for this class of systems. To model these systems many specification languages have been proposed in the literature. One of these is KLAIM: an experimental language specifically designed to program distributed systems consisting of several mobile components that interact through multiple distributed tuple spaces. A stochastic extension of KLAIM, named STOKLAIM, has been proposed to facilitate the incorporation of random phenomena. Moreover, to address key functional aspects of STOKLAIM systems such as distribution awareness, mobility, and security and their integration with performance and dependability guarantees, the temporal logic MoSL has been introduced. In this chapter we show how STOKLAIM and MoSL can be used to specify and verify quantitative properties of distributed systems. These analysis will be performed by relying on statistical model-checking. The use of this relatively new technique permits supporting analysis of large scale systems that, due to the state space explosion problem, cannot be treated via the standard model-checking techniques.
URL: http://onlinelibrary.wiley.com/doi/10.1002/9781119131151.ch2/summary
DOI: 10.1002/9781119131151.ch2
Subject Concurrency Theory
Formal Methods
Model Checking
Stochastic Process Languages
Stochastic Temporal Logics
D.2.4 Software/Program Verification
F.4.1 Mathematical Logic
68N30 Mathematical Aspects of Software Engineering

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