|
|
Laurea Specialistica in
Ingegneria Informatica,
Corso di
Metodi Formali nell'Ingegneria del Software
Edizione dell'a.a. 2007/08
Alcune idee di progetto
In questa pagina verranno elencate alcune idee molto iniziali, utili per nuovi progetti, via via che emergeranno. Queste saranno puntualmente cancellate non appena assegnate ad un gruppo.
Estensione del CASE tool in via di sviluppo per il supporto di vincoli in OCL per la verifica automatica di diagrammi UML delle classi
- Dimensione del gruppo: 3 o 4 persone
- Tempi: entro Aprile 2009
- Capacità richieste: ottime capacità di analisi e di programmazione in Java.
Nel progetto
Fabio D'Aprano, Claudio Di Ciccio.
ReDiA-VeriFInt (Realizzatore Diagrammi Automatico con Verifica Formale Integrata)
Corso di Metodi Formali nell'Ingegneria del Software, Facoltà di Ingegneria, Sapienza Università di Roma. Progetti svolti dagli studenti, 2007/08.
è stata progettata e sviluppata una prima versione di ReDiA-VeriFInt (Realizzatore Diagrammi Automatico con Verifica Formale Integrata), un progetto pilota di CASE, un IDE che permette di assistere 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.
In particolare, il programma permette l'invocazione (per ora solo su richiesta dell'utente) di un dimostratore di teoremi del prim'ordine per verificare proprietà dei diagrammi UML delle classi.
L'idea à quella di estendere il sistema per permettere:
- Il supporto alla definizione di vincoli esterni, in OCL, sui diagrammi UML delle classi;
- Il supporto all'invocazione del dimostratore per la dimostrazione di tesi espresse dall'utente in OCL
- Il supporto alla definizione e gestione dei tipi definiti da utente.
Estensione del CASE tool in via di sviluppo per la verifica automatica di diagrammi UML delle classi mediante Alloy
Questo argomento è stato assegnato ad un gruppo di due studenti che hanno però espresso interesse ad accettare al più altri due componenti.
- Dimensione del gruppo: 3 o 4 persone
- Tempi: entro Aprile 2009
- Capacità richieste: ottime capacità di analisi e di programmazione in Java (in particolare, Swing e programmazione multi-processo/multi-threading).
Nel progetto
Fabio D'Aprano, Claudio Di Ciccio.
ReDiA-VeriFInt (Realizzatore Diagrammi Automatico con Verifica Formale Integrata)
Corso di Metodi Formali nell'Ingegneria del Software, Facoltà di Ingegneria, Sapienza Università di Roma. Progetti svolti dagli studenti, 2007/08.
è stata progettata e sviluppata una prima versione di ReDiA-VeriFInt (Realizzatore Diagrammi Automatico con Verifica Formale Integrata), un progetto pilota di CASE, un IDE che permette di assistere 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.
In particolare, il programma permette l'invocazione (per ora solo su richiesta dell'utente) di un dimostratore di teoremi del prim'ordine per verificare proprietà dei diagrammi UML delle classi.
L'idea à quella di estendere il sistema per permettere:
- Il supporto alla verifica automatica mediante Alloy, compito reso semplice dall'architettura del sistema;
- Il completamento dell'interfaccia grafica per il disegno di diagrammi UML concettuali delle classi e dell'implementazione del livello di collegamento (Control) tra l'interfaccia (View) e la logica applicativa (Model).
- Il supporto all'invocazione automatica, basata su eventi, dei diversi dimostratori di teoremi (ora il sistema permette l'invocazione da parte dell'utente di Prover9, il successore di Otter) su un portafoglio predefinito di tesi da dimostrare (ad es., l'invocazione automatica per dimostrare un'inconsistenza del diagramma dopo averne aggiunto un componente).
Sfruttamento di proprietà strutturali di specifiche di problemi combinatori durante la ricerca
- Dimensione del gruppo: 3 o 4 persone
- Tempi: entro Aprile 2009
- Capacità richieste: ottime capacità logico-matematiche, di analisi, di programmazione in Java e Java/JDBC, e di utilizzo di SQL per la formulazione di query relazionali.
Nel progetto
Michela Angeloni, Junio Valerio Franchi, Piero Cangialosi.
Existential second order logic e sue applicazioni
Corso di Metodi Formali nell'Ingegneria del Software, Facoltà di Ingegneria, Sapienza Università di Roma. Progetti svolti dagli studenti, 2007/08.
è stato presentato il frammento esistenziale della Logica del Secondo Ordine per la specifica dichiarativa di problemi combinatori, e si sono descritte alcune proprietà delle specifiche, come le dipendenze funzionali, che, se note, possono essere sfruttate per rendere il processo di risoluzione più efficiente.
Nell'articolo
Marco Cadoli, Toni Mancini.
Combining Relational Algebra, SQL, Constraint Modelling, and local search.
Theory and Practice of Logic Programming,
7(1--2), pages 37--65, 2007.
è stata poi presentata una estensione del linguaggio SQL (chiamata ConSQL, che può vedersi come una variante di ESO) per la specifica di problemi combinatori, che rende la modellazione a vincoli molto simile al processo di scrivere un insieme di ordinarie query SQL. La risoluzione è poi affidata ad un motore di ricerca locale che si appoggia su un comune DBMS relazionale.
L'idea è quella di analizzare un'altra tipologia di proprietà strutturali delle specifiche, i cosiddetti safe-delay constraint, descritti qui:
Marco Cadoli, Toni Mancini.
Automated reformulation of specifications by safe delay of constraints.
Artificial Intelligence,
170(8--9), pages 779--801, 2006.
e di estendere il sistema ConSQL per:
- permettere all'utente di dichiarare la presenza di tali proprietà nella specifica;
- sfruttare tale conoscenza durante la ricerca, come descritto nell'ultimo articolo.
|
Home page