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.
FlyFast: A mean field model checker / Latella, Diego; Loreti, Michele; Massink, Mieke. - STAMPA. - (2017), pp. 303-309. [10.1007/978-3-662-54580-5_18]
FlyFast: A mean field model checker
LORETI, MICHELE;
2017
Abstract
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.
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
