Courses » LMC1112 » Progetti » Meta-maude: Framework CTMC

Meta-maude: Framework CTMC

  • Progetto di Daniele Bellavista
  • Titolo originale del progetto: Framework per la simulazione e la valutazione di modelli
    CTMC utilizzando Maude e Approximate Probabilistic Model Checking
  • Elaborato nel corso di: Linguaggi e Modelli Computazionali LM (a.a. 2011-2012)
  • Periodo di realizzazione: Febbraio 2012
  • Discusso il:

Sommario

Il progetto consiste nello sviluppo di un framework in Maude per poter definire, simulare e verificare modelli Continous Time Markov Chain (CTMC). Il simulatore deve essere realizzato con l'ausilio del meta-livello di Maude, in modo da poter avere la massima libertà nella definizione di stato del sistema, rate di transizione e condizioni di transizione. La verifica di proprietà del sistema deve avvenire con la tecnica Approximate Probabilistic Model Checking (APMC) per rendere il problema trattabile.

Allegati