PRISMisaprobabilisticmodelchecker,atoolforformalmodellingandanal- ysis of systems that exhibit random or probabilistic behaviour. We extend the language in order to model the Bitcoin system. The tool now supports three dynamic data types: block, ledger and list. As consequence, it is now possible to perform simulations and analyse transient probabilities, i.e. probabilities that are dependent on time, for the Bitcoin protocol. It has been used to under- stand how the system changes during the execution and to analyse the probabilities of reaching an inconsistent state in different settings.
PRISM+
Adele Veschetti;Cosimo Laneve
2020
Abstract
PRISMisaprobabilisticmodelchecker,atoolforformalmodellingandanal- ysis of systems that exhibit random or probabilistic behaviour. We extend the language in order to model the Bitcoin system. The tool now supports three dynamic data types: block, ledger and list. As consequence, it is now possible to perform simulations and analyse transient probabilities, i.e. probabilities that are dependent on time, for the Bitcoin protocol. It has been used to under- stand how the system changes during the execution and to analyse the probabilities of reaching an inconsistent state in different settings.File in questo prodotto:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
