Metodi Formali nell'Ingegneria del Software

Progetti svolti dagli studenti

Torna alla lista dei progetti »

ReDiA-VeriFInt (Realizzatore Diagrammi Automatico con Verifica Formale Integrata)

• Autori: ,

• Categorie: Case tool ReDiA-VeriFInt; Logica del primo ordine; Verifica di algoritmi, programmi, protocolli e hw; Otter/Prover9; Mace2; Dimostratori di teoremi al prim'ordine

Sommario

ReDiA-VeriFInt (Realizzatore Diagrammi Automatico con Verifica Formale Integrata) è il progetto pilota di CASE, un IDE che assisterà il lavoro di analisti, progettisti e programmatori nello sviluppo di applicazioni, tramite la generazione e la gestione di diagrammi UML e codice, lungo tutte le fasi, e con annessa la verifica automatica di opportune proprietà formali, sulla base di quanto realizzato. ReDiA-VeriFInt è il motore per la gestione di Diagrammi UML delle Classi Concettuali. Esso è in grado di memorizzare le informazioni utili alla creazione degli stessi, disegnarli (tramite primitive a basso livello), trasformarli in insiemi di formule della logica del prim'ordine (espresse secondo la sintassi del theorem prover Prover9), verificarne proprietà formali (invocando il dimostratore stesso). ReDiA-VeriFInt, essendo il progetto pilota di una applicazione più estesa, stabilisce un framework valido per ogni tipo di diagramma, basato sul modello MVC, a livello architetturale, e l'integrazione Java/XML, a livello realizzativo.

Materiale prodotto

• Slides

• Relazione

• Codice

Disclaimer: Questo materiale viene offerto gratuitamente ai soli studenti del corso di Metodi Formali nell'Ingegneria del Software del Corso di Laurea Specialistica in Ing. Informatica dell'Università degli Studi di Roma "La Sapienza". E' vietato ogni utilizzo diverso da quello inerente la preparazione dell'esame del suddetto corso, ed in particolare è espressamente vietato il suo utilizzo per qualsiasi scopo commerciale e/o di lucro.

Questo materiale è stato prodotto da un gruppo di studenti del predetto corso, e viene pubblicato senza alcuna garanzia, da parte del docente, circa la sua correttezza e completezza.

Il copyright di questo materiale è detenuto congiuntamente dagli autori e dal docente.
E' permessa la libera copia di tutto il materiale disponibile, purché ne vengano rispettate le condizioni d'uso qui enunciate, ne venga sempre citata la fonte, e venga riportato questo testo.
Gli autori consentono la stampa di questo materiale da parte di società di servizi (ad es. copisterie), purché queste non ne ottengano alcun ricavo oltre quello dovuto alla vendita di semplici fotocopie a prezzi di mercato. Si precisa tuttavia che gli autori ed il docente non percepiscono alcun guadagno dalla diffusione del materiale da parte di chiunque.