Davide Galeotti
abstract
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à.
outcomes
Allegati
