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.
riferimenti