Contributo in atti di convegno, 2017, ENG, 10.1007/978-3-662-54580-5_18

FlyFast: A mean field model checker

Latella D.; Loreti M.; Massink M.

CNR-ISTI, Pisa, Italy; Università di Firenze, Florence, Italy - IMT Alti Studi, Lucca, Italy; CNR-ISTI, Pisa, Italy

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.

International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 303–309, Uppsala, 22-29 April 2017

Keywords

Collective adaptive systems, Discrete time markov chains, Gossip protocols, Mean field model checking, Self-organisation

CNR authors

Massink Mieke, Latella Diego

CNR institutes

ISTI – Istituto di scienza e tecnologie dell'informazione "Alessandro Faedo"