LMC1112 - Progetto Greatspn

Progetto di Chiara Contoli

Titolo originale del Progetto: GreatSPN e MC4CSLTA

Elaborato nel corso di: Linguaggi e Modelli Computazionali LM (a.a. 2010-2011)

Periodo di realizzazione: Ottobre 2013

Discusso il: 28 Novembre 2013

Sommario

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;

Allegati: