Il tool PRISM+

La blockchain è una delle tecnologie più innovative e importanti comparse negli ultimi tempi nel campo dell’informatica. Prism+ è uno strumento che permette di fare analisi probabilistiche ed analizzare il comportamento di modelli di protocolli blockchain. Dopo una breve introduzione, per prima cosa si espone in generale l’argomento della blockchain, enunciando le caratteristiche e gli utilizzi più importanti di questa tecnologia. In seguito viene trattato Prism, strumento che permette di fare analisi su modelli probabilistici, utilizzato per sistemi di diversi campi d’applicazione. Questa sezione si divide in diverse parti: nella descrizione del linguaggio PRISM, che serve per costruire un modello probabilistico analizzabile dal tool; nella spiegazione del linguaggio di specifica delle proprietà necessario per far sì che Prism possa valutare diverse proprietà del modello creato; nella descrizione di un esempio di utilizzo dello strumento Prism, utile per una comprensione diretta del funzionamento del tool. Successivamente si passa alla discussione su Prism+, evoluzione di Prism il cui scopo principale è permettere l’analisi probabilistica di modelli di protocolli blockchain. Questa sezione si divide in due parti: esposizione delle strutture dati aggiunte in Prism+ rispetto a Prism; descrizione delle operazioni possibili tra queste nuove strutture dati. In seguito si riporta un esempio di utilizzo di Prism+. Una breve conclusione pone fine allo scritto.