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 D;Massink M
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.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_369364-doc_123082.pdf
solo utenti autorizzati
Descrizione: FlyFast: a mean field model checker
Tipologia:
Versione Editoriale (PDF)
Dimensione
666.79 kB
Formato
Adobe PDF
|
666.79 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
|
prod_369364-doc_159247.pdf
accesso aperto
Descrizione: postprint version
Tipologia:
Versione Editoriale (PDF)
Dimensione
311.36 kB
Formato
Adobe PDF
|
311.36 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
