Ricerca e Sviluppo

I metodi formali sono tecniche matematicamente rigorose per lo sviluppo e la verifica di sistemi.

Recentemente l’utilizzo congiunto di intelligenza artificiale (AI) e dei metodi formali sta aprendo nuove frontiere, dalla dimostrazione automatica di teoremi matematici alla verifica di sistemi ingegneristici su larga scala.

Utilizzare i metodi formali nelle varie fasi di sviluppo e di verifica assicura la massima qualità e validità del sistema, mentre l’utilizzo dell’AI velocizza il processo di creazione dei test.

La nostra esperienza ci ha consentito di sperimentare con successo l’utilizzo combinato di Metodi Formali e Intelligenza Artificiale per sviluppare Server e tool MCP personalizzati che consentono ai modelli AI fine-tuned di interagire direttamente con i sistemi esistenti.

I metodi formali sono tecniche matematicamente rigorose per lo sviluppo e la verifica di sistemi.

Recentemente l’utilizzo congiunto di intelligenza artificiale (AI) e dei metodi formali sta aprendo nuove frontiere, dalla dimostrazione automatica di teoremi matematici alla verifica di sistemi ingegneristici su larga scala.

Utilizzare i metodi formali nelle varie fasi di sviluppo e di verifica assicura la massima qualità e validità del sistema, mentre l’utilizzo dell’AI velocizza il processo di creazione dei test.

Nella fase di verifica, l’intelligenza artificiale permette di creare test basandosi sui requisiti formali e una documentazione tecnica attraverso Retrieval-Augmented Generation (RAG), e di interagire direttamente con strumenti di verifica formale, come SAT solver (Boolean Satisfiability Problem) sfruttando l’architettura Model Context Protocol (MCP) e analizzare edge cases che potrebbero altrimenti sfuggire ad un’analisi manuale.

Nella fase di sviluppo, i modelli AI specializzati propongono implementazioni già conformi alle specifiche formali, riducono drasticamente i cicli di correzione-verifica, e adattano automaticamente il codice a requisiti mutevoli mantenendo le garanzie di correttezza.