PolyVer: Un Approccio Composizionale per la Modellazione e Verifica di Sistemi Poliglotta

Informazioni Fondamentali

• ID Articolo: 2503.03207
• Titolo: PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
• Autori: Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia
• Classificazione: cs.PL (Linguaggi di Programmazione)
• Data di Pubblicazione/Conferenza: Formal Methods in Computer-Aided Design 2025
• Link Articolo: https://arxiv.org/abs/2503.03207

Riassunto

I sistemi software poliglotta (polyglot systems) sono composti da programmi implementati in molteplici linguaggi di programmazione, tuttavia i verificatori di programmi esistenti sono tipicamente personalizzati per un singolo linguaggio. Per verificare sistemi poliglotta, è generalmente necessario tradurli in un linguaggio di verifica comune o in una rappresentazione formale. Questo articolo propone PolyVer, un approccio alternativo che esegue la verifica poliglotta direttamente utilizzando tecniche di astrazione, ragionamento composizionale e sintesi. PolyVer modella sistemi poliglotta come modelli formali di sistemi di transizione, dove le funzioni di aggiornamento relative alle transizioni sono implementate nel linguaggio target (come C o Rust). Per eseguire la verifica, PolyVer connette il model checker del sistema di transizione con verificatori specifici del linguaggio attraverso contratti di precondizione/postcondizione delle funzioni di aggiornamento. Questi contratti vengono generati automaticamente tramite sintesi guidata dalla sintassi o oracoli di sintesi basati su modelli linguistici di grandi dimensioni, e verificati dai verificatori specifici del linguaggio.

Contesto di Ricerca e Motivazione

Definizione del Problema

I sistemi software moderni adottano sempre più frequentemente architetture poliglotta, come i framework ROS2 e Lingua Franca che consentono agli sviluppatori di scegliere il linguaggio di programmazione più appropriato per ciascun componente. Tuttavia, questa flessibilità introduce sfide di verifica:

1. Differenze Semantiche tra Linguaggi: Diversi linguaggi di programmazione possiedono sintassi e semantica differenti, come la funzione saturating_add di Rust che satura al valore massimo in caso di overflow, mentre l'addizione in C può causare wrapping.
2. Limitazioni dei Verificatori Esistenti: La maggior parte dei verificatori di programmi (come CBMC per C, Kani per Rust) sono progettati specificamente per un singolo linguaggio e non possono gestire direttamente sistemi poliglotta.
3. Complessità della Traduzione: Tradurre un intero sistema poliglotta in un singolo linguaggio di verifica richiede il supporto della sintassi e della semantica complete di tutti i linguaggi, il che è proibitivo per i linguaggi moderni.

Importanza della Ricerca

La crescente complessità dei sistemi poliglotta aumenta il rischio di difetti software, e nei settori critici per la sicurezza (come i veicoli autonomi e l'aerospaziale), è necessaria la verifica formale per fornire garanzie forti, piuttosto che affidarsi esclusivamente a metodi incompleti come i test.

Limitazioni degli Approcci Esistenti

• Metodi di Traduzione Monolitica: Richiedono lo sviluppo di un'infrastruttura compilatore completa per ogni linguaggio
• Difficoltà nel Preservare la Semantica: È difficile catturare fedelmente tutte le costruzioni specifiche del linguaggio sorgente nel linguaggio di verifica target
• Problemi di Scalabilità: I problemi di verifica generati possono diventare eccessivamente grandi

Contributi Principali

1. Formalizzazione del Problema di Verifica Poliglotta: Formalizzazione sistematica per la prima volta del problema di verifica poliglotta, con proposta di una soluzione composizionale che integra molteplici verificatori specifici del linguaggio.
2. Sintesi Automatica di Contratti: Proposta di un metodo automatico per la sintesi e il raffinamento di contratti di precondizione/postcondizione utilizzando un linguaggio intermedio e cicli CEGIS-CEGAR, con supporto per sintesi guidata dalla sintassi e oracoli di sintesi basati su modelli linguistici di grandi dimensioni.
3. Implementazione dello Strumento: Implementazione dello strumento PolyVer basato su UCLID5, con supporto per C e Rust attraverso i verificatori CBMC e Kani, dimostrando che gli oracoli di sintesi basati su LLM superano i metodi di sintesi puramente simbolici.
4. Studi di Caso e Valutazione: Sviluppo di un verificatore per il linguaggio di coordinamento Lingua Franca, verifica di sistemi poliglotta contenenti processi C e Rust, nonché frammenti di linguaggio C non supportati da lavori precedenti.

Dettagli del Metodo

Definizione del Compito

Input: Modello poliglotta M = (Q,V,I₀,T,F) e proprietà del sistema φ Output: Risultato di verifica (pass/fail) e possibile traccia di controsempio Obiettivo: Determinare se M ⊨ φ è valido

Dove:

• Q: Insieme di stati
• V: Insieme di variabili tipizzate
• I₀: Insieme di stati iniziali
• T: Insieme di transizioni di stato
• F: Insieme di procedure

Architettura del Modello

1. Macchina a Stati Estesa (ESM)

PolyVer modella sistemi poliglotta come macchine a stati estese, dove:

• Gli stati sono composti da stati e assegnazioni di variabili
• Le transizioni sono associate a condizioni di guardia e relazioni di aggiornamento
• Le relazioni di aggiornamento sono specializzate in sequenze di chiamate di procedure

2. Linguaggio Contrattuale Intermedio L*

L'innovazione chiave è l'introduzione del linguaggio intermedio L* come "collante" tra diversi linguaggi:

• I contratti sono scritti in L*
• Vengono trasformati in linguaggi concreti attraverso la compilazione semantica-preservante compL
• Evita la complessità della traduzione completa del linguaggio

3. Metodo Ibrido CEGIS-CEGAR

Il nucleo dell'algoritmo è un ciclo iterativo a due livelli:

Ciclo CEGAR Esterno:

1. Costruisce un modello astratto M' utilizzando i contratti correnti
2. Il model checker verifica M' ⊨ φ
3. Se fallisce, controlla se il controsempio è spurio
4. Se spurio, raffina il contratto; altrimenti segnala il controsempio reale

Ciclo CEGIS Interno:

1. L'oracolo di sintesi genera contratti candidati
2. Il verificatore di oracolo controlla la validità del contratto
3. Se non valido, aggiunge esempi positivi e risintesi

Punti di Innovazione Tecnica

1. Strategia di Verifica Composizionale

A differenza della traduzione monolitica, PolyVer adotta una strategia "divide et impera":

• Utilizza contratti per astrarre procedure individuali
• I verificatori specifici del linguaggio verificano la validità dei contratti
• Il model checker verifica le proprietà a livello di sistema

2. Generazione Automatica di Contratti

Supporta molteplici oracoli di sintesi:

• Sintetizzatore Basato su LLM: Utilizza prompt con catena di pensiero e DSL Python
• Sintetizzatore SyGuS/SyMO: Codifica il problema come problema di programmazione per esempi

3. Controllo di Spuriosità

Controlla la raggiungibilità della traccia di controsempio verificando {V = d} C {V' ≠ d'}, distinguendo tra controsempi reali e spuri.

Configurazione Sperimentale

Dataset

1. Benchmark LFVerifier: 22 programmi Lingua Franca con sintassi C limitata
2. Esempi LF Completi: Controllore LED, robot arrampicatore, controllore di assetto satellitare e altri sistemi embedded
3. Sistemi Poliglotta: Programmi LF misti C/Rust, applicazioni ROS2, programmi con chiamate FFI

Metriche di Valutazione

• Numero di iterazioni di sintesi (IS: iterazioni CEGIS, AR: iterazioni CEGAR)
• Tempo di esecuzione (SOT: tempo oracolo di sintesi, VOT: tempo verificatore oracolo, UT: tempo UCLID5)
• Tasso di successo della verifica

Metodi di Confronto

Confronto con LFVerifier15, l'unico strumento noto per la verifica automatica end-to-end di programmi LF.

Dettagli di Implementazione

• Utilizzo di OpenAI o1-mini come sintetizzatore LLM, con 3 query parallele per procedura
• CBMC-6.3.1, Kani-0.56.0, z3-4.8.7 come backend di verifica
• Macchina Intel Core i9 a 3.7GHz con 62GB RAM

Risultati Sperimentali

Risultati Principali

RQ1: Confronto con Lavori di Verifica LF Esistenti

Su 22 benchmark:

• PolyVer verifica con successo tutti i benchmark, mentre LFVerifier non riesce a verificare l'esempio TrafficLight
• 18 benchmark sintetizzano correttamente i contratti in un singolo ciclo CEGIS, con tempo medio di 37 secondi
• Sebbene il tempo di esecuzione totale sia più lento (principalmente dominato dal tempo di sintesi dei contratti), fornisce miglioramenti qualitativi significativi

RQ2: Gestione di Esempi LF Completi

Verifica con successo sistemi embedded contenenti codice C completo:

• Controllore LED: 1 procedura, 123 righe di codice C, 31.0 secondi di tempo di sintesi
• Robot Arrampicatore: 12 procedure, 75 righe di codice C/Rust, 685.4 secondi di tempo di sintesi
• Controllore Satellitare: 6 procedure, 424 righe di codice C, 729.0 secondi di tempo di sintesi

RQ3: Verifica di Sistemi Poliglotta

Verifica di veri sistemi poliglotta:

• Programmi LF misti C/Rust
• Applicazioni di servizi ROS2
• Programmi con chiamate FFI tra linguaggi

Scoperte Importanti

1. LLM Superiore ai Metodi Simbolici: I risolutori SyGuS/SyMO richiedono numerose iterazioni CEGAR e spesso non terminano
2. Sfide nella Sintesi di Contratti: Le procedure con flusso di controllo complesso e dipendenze di dati richiedono più iterazioni
3. Verifica Pratica: Capace di gestire codice implementativo reale piuttosto che esempi giocattolo

Lavori Correlati

Verifica di Sistemi Poliglotta

• Metodi di Traduzione Manuale: Cook et al. traducono codice assembly in C per verificare l'hypervisor Xen
• Traduzione Automatica di Frammenti: LFVerifier traduce automaticamente frammenti C in linguaggio di verifica
• Metodi Black-Box: Inferiscono riassunti dal comportamento di input-output

Verifica Composizionale

• La verifica composizionale basata sulla logica di Hoare è ampiamente applicata a programmi monolingue su larga scala
• Utilizza interpretazione astratta e CEGAR per automatizzare l'apprendimento di precondizioni/postcondizioni

Inferenza di Contratti

• Metodi di inferenza di contratti guidati da proprietà
• Risolutori di clausole Horn vincolate
• Applicazioni recenti di LLM nell'apprendimento di specifiche

Conclusioni e Discussione

Conclusioni Principali

1. PolyVer risolve con successo le sfide chiave della verifica di sistemi poliglotta
2. L'approccio composizionale evita la complessità della traduzione completa del linguaggio
3. La sintesi automatica di contratti rende il metodo pratico
4. Gli oracoli di sintesi basati su LLM superano i metodi simbolici tradizionali

Limitazioni

1. Terminazione: L'algoritmo non garantisce la terminazione, dipendendo dalla qualità dell'oracolo di sintesi
2. Supporto Linguistico: Attualmente supporta solo C e Rust, richiedendo lo sviluppo di oracoli di verifica per altri linguaggi
3. Espressività dei Contratti: L'espressività del linguaggio intermedio L* limita la complessità delle proprietà verificabili
4. Scalabilità: Il tempo di sintesi dei contratti per sistemi di grandi dimensioni potrebbe diventare un collo di bottiglia

Direzioni Future

1. Estensione a altri sistemi software distribuiti poliglotta e sistemi robotici
2. Applicazione alla verifica formale della traduzione di codice (come la traduzione da C a Rust)
3. Miglioramento dell'efficienza e dell'accuratezza della sintesi di contratti
4. Supporto per proprietà di logica temporale più complesse

Valutazione Approfondita

Punti di Forza

1. Importanza del Problema: La verifica di sistemi poliglotta è un problema pratico e importante
2. Innovazione del Metodo: La combinazione di verifica composizionale e sintesi automatica di contratti è innovativa
3. Fondamenti Teorici: Definizioni formali chiare e garanzie di correttezza esplicite
4. Valore Pratico: Capace di gestire sistemi reali piuttosto che esempi giocattolo
5. Implementazione dello Strumento: Fornisce un'implementazione dello strumento utilizzabile

Insufficienze

1. Overhead di Prestazioni: Il tempo di sintesi dei contratti è considerevole, potendo limitare l'applicazione pratica
2. Copertura Linguistica: Attualmente supporta solo C e Rust, con estensibilità ancora da verificare
3. Benchmark Limitati: Sebbene includa esempi reali, la scala è relativamente piccola
4. Dipendenza da LLM: Dipende da servizi LLM commerciali, potendo influenzare la riproducibilità

Impatto

1. Contributo Accademico: Apre una nuova direzione di ricerca per la verifica di sistemi poliglotta
2. Valore Pratico: Fornisce uno strumento di verifica per sistemi poliglotta critici per la sicurezza
3. Ispirazione Tecnica: L'idea di utilizzare contratti come interfaccia tra linguaggi ha valore universale

Scenari Applicabili

1. Sistemi Embedded: Sistemi real-time misti C/Rust
2. Sistemi Distribuiti: Framework multilingue come ROS2 e gRPC
3. Applicazioni Critiche per la Sicurezza: Sistemi che richiedono garanzie di verifica formale
4. Integrazione di Sistemi Legacy: Sistemi con codice nuovo e vecchio mescolato

Bibliografia

L'articolo cita 50 lavori correlati, coprendo molteplici aree di ricerca inclusi sistemi poliglotta, verifica formale, inferenza di contratti e sintesi guidata dalla sintassi, fornendo una base teorica solida per la ricerca.

Valutazione Complessiva: Questo è un articolo di ricerca di alta qualità che affronta un problema importante e pratico. Il metodo è innovativo, gli esperimenti sono completi e l'implementazione dello strumento è completa. Sebbene ci sia ancora spazio per miglioramenti in termini di prestazioni e scalabilità, l'articolo fornisce contributi significativi al campo della verifica di sistemi poliglotta.