Courses » LMC1112 » Progetti » Progetto MC LTL

MODEL CHECKER LTL

Progetto di: Manuel Bartolini, Luca Guerra

Titolo originale del progetto: Model Checker LTL

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

Periodo di realizzazione: Dicembre 2011 - Gennaio 2012

Discusso il: 15 Febbraio 2012

Sommario

Scopo del progetto è stata la realizzazione di un Model Checker che si occupasse della verifica di regole LTL su un modello dato in ingresso. Per fare questo è stata realizzata una libreria, quasi interamente scritta in Prolog, completa di tutte le funzioni necessarie per effettuare il checking.Inoltre viene fornito un manuale (in inglese) per aiutare nella comprensione del linguaggio che l'utente dovrà usare per sottoporre il codice delle proprie applicazioni al MC. Gli allegati sottostanti comprendono: un file jar in cui la libreria è stata aggiunta a quelle disponibili con il tool tuProlog per testare subito l'applicazione, i codici sorgenti, il file .class della libreria, il manuale utente,la relazione del progetto e inoltre un file pdf contenente i benchmark utilizzati durante lo sviluppo.

Allegati: