Software and System Verification

Gruppo di ricerca

• Agostino Cortesi
• Pietro Ferrara
• Paolo Falcarin
• Maikel Perez Lazaro Gort
• Gianluca Caiazza
• Alvise Spanò
• Luca Olivieri
• Luca Negrini

Collaboratori

• Souvick Das
• Raunak Bag
• Badaruddin Chachar
• Giacomo Zanatta
• Giacomo Boldini
• Teodors Lisovenko
• Aradhita Mukherjee
• Vincenzo Arceri (Università di Parma)

Sito web: ssv.dais.unive.it

Collaborazioni

• Ecole Normale Superieure Paris
• ETH Zurich
• University of Calcutta
• University of Patna
• Meta
• Università di Verona
• Università di Padova
• Università di Cagliari

Pubblicazioni

• G. Caiazza, T. Lisovenko, P. Ferrara, F. Berti, F. Ferrari, A. Zaupa, G. Zhang: “From Legacy to Intelligent IIoT Systems: Automation, Scalability and Elasticity”, Proceedings of the IEEE 22nd International Conference on Software Architecture (ICSA 2025), Odense, Denmark, April 3‑5, 2025
• Pietro Ferrara, Vincenzo Arceri, Agostino Cortesi: Challenges of software verification: the past, the present, the future. Int. J. Softw. Tools Technol. Transf. 26(4): 421-430 (2024)
• Giacomo Zanatta, Gianluca Caiazza, Pietro Ferrara, Luca Negrini, Ruffin White Automating ROS2 Security Policies Extraction through Static Analysis , Proceedings of IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) (2024)
• Luca Olivieri, Luca Negrini, Vincenzo Arceri, Fabio Tagliaferro, Pietro Ferrara, Agostino Cortesi, Fausto Spoto: Information Flow Analysis for Detecting Non-Determinism in Blockchain. ECOOP 2023: 23:1-23:25
• Mandira Roy, Raunak Bag, Novarun Deb, Agostino Cortesi, Rituparna Chaki, Nabendu Chaki: SCARS: Suturing wounds due to conflicts between non-functional requirements in autonomous and robotic systems. Softw. Pract. Exp. 54(5): 759-795 (2024)
• Souvick Das, Novarun Deb, Nabendu Chaki, Agostino Cortesi: Driving the Technology Value Stream by Analyzing App Reviews. IEEE Trans. Software Eng. 49(7): 3753-3770 (2023)

Riconoscimenti

• La spin-off SecuraFactors ha vinto la SmartCup Veneto 2020 per il settore ICT

Progetti di ricerca

Progetti in corso

• SUPREME (RIR): Il progetto multi-RIR SUPREME “Sistemi Umano centrici per Prodotti e pRocEssi Manufatturieri Evoluti” mira a progettare ed implementare sistemi avanzati e sicuri per il monitoraggio di linee di produzione/prodotti, per l’ottimizzazione del processo e della sua efficienza, la rilevazione di guasti e la manutenzione, il controllo di qualità e la tracciabilità. Utilizzando tecnologie ICT, in continuità con i percorsi già intrapresi nella visione di Industria 4.0, si intende realizzare sistemi decisionali avanzati di supporto all’operatore che ne aumentano l'operatività e la centralità all’interno delle varie funzioni aziendali, nella direzione di una visione industriale più efficiente e sostenibile.

• SATCO (RIR): Il progetto SATCO nasce all’interno della Rete Innovativa Regionale “Air – Aerospace Innovation and Research”. L’obiettivo principale del progetto è sviluppare un satellite in grado di adattarsi dinamicamente alle missioni, grazie all’uso dell’intelligenza artificiale. Questa tecnologia rende il satellite un sistema intelligente e riconfigurabile, capace di evolversi in base alle esigenze operative, superando i limiti dei satelliti tradizionali. L’intero progetto si articola in due fasi: inizialmente verrà realizzato un “flatsat”, un modello di satellite non operativo che consentirà di testare le tecnologie critiche. Successivamente, si procederà all’integrazione dei sistemi per completare un satellite pronto per il volo, dotato di tecnologie di controllo avanzato e di sistemi di alimentazione e propulsione.

• Ecodigify (Erasmus+): EcoDigify mira ad avviare un programma universitario interdisciplinare orientato al futuro che affronterà le sfide multidimensionali della promozione della sostenibilità nell'uso e nello sviluppo delle tecnologie digitali. Ciò sarà ottenuto migliorando la conoscenza degli educatori sulla digitalizzazione sostenibile e fornendo agli studenti la conoscenza

• SERICS (PNRR Partenariato esteso): SERICS - Security and Rights in CyberSpace è un parteneriato esteso che coinvolge diverse università italiane e si concentra sulle attività di sicurezza informatica. Il laboratorio SSV è coinvolto nell'attività di Spoke 6 su Software and Platform Security. L'obiettivo di questo spoke è duplice: (i) fornire un ecosistema in cui gli sviluppatori di software possano facilmente ragionare sulla sicurezza del software e (ii) fornire soluzioni innovative per proteggere la supply chain del software, incluso il processo di gestione e sviluppo del software.
  Sito web: https://serics.eu/

• iNEST (PNRR Ecosistemi dell'innovazione): iNEST - Interconnected Nord-Est Innovation Ecosystem è un ecosistema dell'innovazione il cui modello si basa sull'uso estensivo delle tecnologie dell'informazione e della comunicazione e sulla digitalizzazione, e mira allo sviluppo di tecnologie innovative per il benessere delle persone e la diffusione della cultura e della crescita economica e imprenditoriale. Il laboratorio SSV è coinvolto nelle attività di Spoke 3 su "Green and digital transition for advanced manufacturing technology".
  Sito web: https://www.consorzioinest.it/

Progetti terminati

• 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/ [ENG]

• 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/

• 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.

• 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".

• 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.