Software and System Verification
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/848x174/banner_SeSV_848x174.jpg)
Il laboratorio è specializzato nella progettazione e applicazione di tecniche basate su metodi formali per la specifica e la verifica di affidabilità e sicurezza di sistemi software. Le tecniche utilizzate si applicano al codice sorgente contribuendo a un miglioramento del processo di sviluppo in modo sicuro (DevSecOps), in un’ottica di assicurazione di qualità e di certificazione dei sistemi software.
Il laboratorio, attraverso i suoi partecipanti, ha fondato lo spin-off SecuraFactors, specializzato nella verifica di sicurezza di sistemi robotici, ed è parte attiva di progetti di trasferimento tecnologico della RIR Improvenet.
Collaboratori
- Raunak Bag
- Gianluca Caiazza
- Luca Negrini
- Martina Olliaro
- Maikel Lazaro Perez Gort
- Alvise Spanò
- Ruffin White
Sito web: ssv.dais.unive.it
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/Lab_SeSV_600x362.jpg)
Collaborazioni
- Ecole Normale Superieure Paris
- ETH Zurich
- University of Calcutta
- University of Patna
- Meta
- Università di Verona
- Università di Padova
- Università di Cagliari
Pubblicazioni
- Vincenzo Arceri, Martina Olliaro, Agostino Cortesi, Isabella Mastroeni: Completeness of string analysis for dynamic languages. Information and Computation 281: 104791 (2021)
- Pietro Ferrara, Amit Kr Mandal, Agostino Cortesi, Fausto Spoto: Static analysis for discovering IoT vulnerabilities. Int. J. Softw. Tools Technol. Transf. 23(1): 71-88 (2021)
- Maikel Lázaro Pérez Gort, Martina Olliaro, Agostino Cortesi, Claudia Feregrino Uribe: Semantic-driven watermarking of relational textual databases. Expert Systems with Application 167: 114013 (2021)
- Angshuman Jana, Raju Halder, Kalahasti Venkata Abhishekh, Sanjeevini Devi Ganni, Agostino Cortesi: Extending Abstract Interpretation to Dependency Analysis of Database Applications. IEEE Transactions on Software Engineering 46(5): 463-494 (2020)
- Pietro Ferrara, Agostino Cortesi, Fausto Spoto: From CIL to Java bytecode: Semantics-based translation for static analysis leveraging. Sci. Comput. Program. 191: 102392 (2020)
- Ruffin White, Gianluca Caiazza, Agostino Cortesi, Young Im Cho, Henrik I. Christensen: Black Block Recorder: Immutable Black Box Logging for Robots via Blockchain. IEEE Robotics Automation Letters 4(4): 3812-3819 (2019)
Riconoscimenti
- La spin-off SecuraFactors ha vinto la SmartCup Veneto 2020 per il settore ICT
Progetti di ricerca
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/Families_Share_600x362.jpg)
Families_Share: Socializing and sharing time for work/ life balance through digital and social innovation
Families_Share è un progetto H2020 che cerca di supportare le famiglie, con particolare riferimento a quelle a basso reddito, nelle pratiche di time sharing per le loro attività di childcare, genitorialità, dopo-scuola e tempo libero offrendo loro soluzioni bottom-up e una piattaforma co-progettata, attraverso l'attivazione di sette City Labs in sette diverse città europee. A tal fine, il progetto si baserà su pratiche correnti già attive a livello di quartiere che stanno sfruttando il mutuo soccorso e il sostegno tra famiglie, come le banche del tempo, le social streets e le reti auto-organizzate dei genitori, cercando di sfruttare il potenziale delle reti ICT e delle tecnologie mobili per accrescere l'efficacia degli approcci partecipativi dal basso.
Sito web: http://www.families-share.eu/
Facebook: https://www.facebook.com/familiesShare/
Twitter: https://twitter.com/Families_Share
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/EQUAL-IST_600x362.jpg)
EQUAL-IST: Gender Equality Plans for Information Sciences and Technology Research Institutions
Il Progetto EQUAL-IST ha l'obiettivo di sostenere processi di cambiamento strutturale per l'uguaglianza di genere in 7 Facoltà -Dipartimenti di Informatica e Sistemi e Tecnologie dell'Informazione in Finlandia, Germania, Italia, Lituania, Portogallo, Ucraina. Le Università partner attraverseranno una prima fase di analisi e audit interno finalizzato a fotografare l'esistente e valutare in che misura diseguaglianze/stereotipi di genere siano presenti a livello di gestione delle risorse umane e organizzazione del lavoro, processi decisionali, ma anche ricerca, servizi agli studenti e comunicazione istituzionale. I dati raccolti saranno oggetto di un confronto interno aperto a personale accademico e amministrativo e agli studenti, attraverso l'uso di una piattaforma di crowdsourcing che servirà a co-progettare Piani di Azione per l'Uguaglianza di Genere in ognuna delle istituzioni coinvolte. I Piani d'Azione comprenderanno diversi interventi che saranno testati e monitorati nei singoli contesti fino alla chiusura del progetto. Attività di disseminazione e networking con altre Università in Europa, di sinergia con Euraxess- HRS4R e di elaborazione di scenari di sostenibilità per i Piani di Azione sull'Uguaglianza di Genere completano il progetto.
Sito web: http://equal-ist.eu/
Facebook: https://www.facebook.com/EQUALISTproject/
Twitter: https://twitter.com/EQUALISTproject
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/ADMIIN-4D_600x362.jpg)
ADditive Manufacturing & INdustry 4.0 as innovation Driver - ADMIN 4D
Il progetto ADMIN 4D coinvolge diverse tecnologie abilitanti nell'ambito della specializzazione intelligente "Smart Manufacturing". Si sviluppa attraverso una collaborazione inedita tra esponenti di rilievo nell'ambito della ricerca e dell’implementazione industriale delle diverse tecnologie interessate: tecnologia additiva (nota come stampa 3D), ingegneria dei materiali, sensoristica in ambiente Internet of Things e meccanica/meccatronica.
L'obiettivo del progetto è lo sviluppo di un sistema innovativo che consenta la raccolta e l'elaborazione, mediante algoritmi sviluppati ad hoc, di informazioni tecnico-chimiche provenienti dai nuovi materiali e leganti usati nei prodotti e dalle strumentazioni di produzione (stampa 3D) brevettati dai partner di progetto e tutt'oggi oggetto di attività di R&D orientate al loro perfezionamento e diffusione sul territori.
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/VIR2EM_600x362.jpg)
VIR2EM - VIrtualization and Remotization for Resilient and Efficient Manufacturing
Il progetto VIR2EM (VIrtualization and Remotization for Resilient and Efficient Manufacturing), propone di utilizzare tecnologie di virtualizzazione per processi, sistemi e risorse per favorire la remotizzazione nelle reti industriali.
Nell'ambito della Smart Manufacturing, le soluzioni software e infrastrutturali per l'Internet of Things necessitano di analisi e sviluppo degli aspetti fondamentali associati alla sicurezza informatica, al miglioramento dell'usabilità, e dell'impatto su modelli di business e sulle organizzazioni, al fine di applicare tecniche dal mondo dell'Information Technology (IT) all’ambito dell'Operation Technology (OT).
Gli obiettivi del progetto includono:
1) massimizzare l'efficienza dei sistemi produttivi in normali condizioni operative;
2) mantenere l'operatività in caso di emergenza;
3) facilitare la ripartenza delle operazioni a seguito di emergenze, garantendo flessibilità e capacità predittiva.
Per fare ciò, il progetto mira, tra l'altro, allo sviluppo di strumenti di monitoraggio, supervisione remota e ottimizzazione delle operazioni di servizio e post vendita, con un focus su:
1) metodologie interpretabili;
2) metodologie per l’utilizzo del fog computing;
3) approcci di "lifelong learning".
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/Specifiche_Formali_600x362.jpg)
MIUR-MAE Italia-India - Specifiche Formali per Sistemi Software Sicuri
L'obiettivo del progetto è studiare se le politiche di sicurezza di sistemi software critici possano essere formalmente integrate nelle tecniche di specifica dei requisiti usando metodi formali, per individuare ambiguità e inconsistenze già nella fase di specifica del ciclo di vita del software. A tal fine applicheremo tecniche lightweight di validazione e verifica per "mettere in sicurezza" il software già in fase di ingegneria dei requisiti. In particolare applicheremo linguaggi di modellazione come Event-B e iSTAR per specificare e analizzare i requisiti così che la progettazione del software possa essere conformata a criteri di sicurezza. Complessivamente, il progetto risponde all'esigenza di utilizzare tecniche matematiche con solido fondamento teorico per validare aspetti di sicurezza degli applicativi software.
Last update: 28/08/2024