abstract
Lo scopo di questo progetto è sperimentare l'utilizzo di due tool:
- GreatSPN: consente la modellazione di sistemi tramite il formalismo del linguaggio grafico delle reti di Petri;
- MC4CSLTA: è un model checker probabilistico per la logica stocastica CSLTA che esegue il modeling formale e l'analisi quantitativa di sistemi , specificati come catene di Markov Tempo Continue (CTMCs).
I due tool sono stati sperimentati su tre casi di studio:
- sistema a coda: si suppone vi siano due classi di utenza, una più prioritaria dell'altra;
- protocollo TCP: si suppone vi siano un numero finito di Client e Server, in grado di effettuare apertura e chiusura attiva/passiva della connessione;
- variante del caso precedente: si valuta il caso in cui non tutte le richieste di connessione vengono soddisfatte
outcomes
Allegati:
