Courses » LMC1112 » Progetti » Model checking per le reti di Petri colorate

MODEL CHECKING PER LE RETI DI PETRI COLORATE

Progetto di Davide Galeotti

Titolo originale del progetto:  Reti di Petri colorate : realizzazione di un traduttore Prolog/Promela per l’analisi con il model checker Spin

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

Periodo di realizzazione:  Gennaio - Febbraio 2012

Discusso il:  6 Marzo 2012

Sommario
Scopo del progetto è stato quello di sfruttare le capacità del software open source Spin come model checker per la verifica di proprietà LTL su modelli costruiti con il formalismo delle reti di Petri colorate (CPN). Tutto ciò è stato realizzato definendo un modello Promela per le CPN, alcuni predicati Prolog per la rappresentazione concisa delle CPN ed un traduttore che generasse il codice Promela dalla teoria Prolog. Grazie a Spin è stato possibile utilizzare il codice generato per simulare la propria CPN e per verificare formalmente proprietà.

Allegati