PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., Loreti M., Massink M. FlyFast: a mean field model checker. In: TACAS 2017 - International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Uppsala, Sweden, 22-29 April 2017). Proceedings, pp. 303 - 309. Axel Legay, Tiziana Margaria (eds.). (Lecture Notes in Computer Science, vol. 10206). Springer, 2017.
 
 
Abstract
(English)
We present FlyFast, a recently introduced on-the-fly mean field model checker for the verification of time-dependent probabilistic properties of individual objects in the context of large populations. An example of its use is illustrated analysing a push-pull gossip protocol. Such protocols form the basis on top of which many smart collective adaptive systems are built. Typical properties are the replication of a fresh data element throughout a network, the coverage of the network, and the time to convergence.
URL: http://link.springer.com/chapter/10.1007/978-3-662-54580-5_18
DOI: 10.1007/978-3-662-54580-5_18
Subject Probabilistic model-checking
On-the-fly model-checking
Mean-field approximation
Discrete time Markov chains
Software Tools
B.8.2 PERFORMANCE AND RELIABILITY. Performance Analysis and Design Aids
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification
F.1.2 COMPUTATION BY ABSTRACT DEVICES. Modes of Computation
G.3 PROBABILITY AND STATISTICS
39-XX Difference and functional equations
60Jxx Markov processes


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