Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems

1. Il Problema

I Sistemi Cyber-Fisici (CPS), come veicoli autonomi, robot agricoli e dispositivi medici (es. pacemaker), operano in ambienti critici per la sicurezza dove affidabilità e correttezza sono essenziali. La Signal Temporal Logic (STL) è lo standard de facto per specificare proprietà temporali su segnali continui in questi sistemi. Tuttavia, la verifica statica delle proprietà STL è indecidibile in generale, poiché richiede di valutare formule su intervalli temporali continui (reali), il che comporta un numero infinito di punti di controllo.

Le alternative esistenti presentano limiti significativi:

• Verifica a runtime: Non garantisce la sicurezza prima della distribuzione e non esplora tutti i percorsi di esecuzione possibili.
• Sintesi del controllore: Spesso incontra problemi di scalabilità per sistemi complessi.
• Approssimazione: Le tecniche di sovrastima (over-approximation) possono gestire solo le proprietà di sicurezza ("niente di brutto accade mai"), ma non quelle di vivacità ("qualcosa di buono accade prima o poi").

Il paper affronta la sfida di rendere decidibile la verifica statica sia per le proprietà di sicurezza che per quelle di vivacità, mantenendo un collegamento rigoroso con il comportamento continuo del sistema.

2. Metodologia: Synchronous Signal Temporal Logic (SSTL)

Gli autori propongono SSTL, un frammento decidibile della STL, basato su un approccio sincrono e discreto. La metodologia si articola in tre fasi principali:

A. Discretizzazione del Tempo e Ipotesi di Invarianza del Segnale (SIH)

Il tempo continuo ($t \in \mathbb{R}_{\ge 0}$) viene mappato su istanti discreti (ticchettii o ticks) tramite un operatore di proiezione $[t] = \lfloor t / \Delta t \rfloor$.
Il cuore della metodologia è l'Ipotesi di Invarianza del Segnale (Signal Invariance Hypothesis - SIH). Questa ipotesi afferma che il valore di un segnale rimane costante all'interno di un singolo intervallo di tick (tra due campioni consecutivi).

• Condizione di validità: L'SIH è valida se la frequenza di campionamento soddisfa il criterio di Nyquist, garantendo che non vi siano cambiamenti significativi nel segnale continuo tra due campioni che verrebbero persi.
• Implicazione: Sotto SIH, la verifica su una traccia discreta è equivalente alla verifica sulla traccia continua originale.

B. Sintassi e Semantica di SSTL

SSTL definisce una sintassi che opera su segnali discreti $w_d: \mathbb{N}_{\ge 0} \to \mathbb{R}^n$. Gli operatori temporali (come Until, Eventually, Always) sono ridefiniti su intervalli discreti $[[a], [b]]$.

• Viene dimostrato un teorema di equivalenza: se un segnale continuo soddisfa la SIH, allora una formula STL $\varphi$ è soddisfatta se e solo se la sua controparte SSTL $[\varphi]$ è soddisfatta sulla traccia discretizzata.

C. Traduzione in LTLP e Verifica con SPIN

Per rendere la verifica pratica e automatizzata, gli autori traducono le formule SSTL in LTLP (Linear Temporal Logic with Predicates).

• Traduzione: Gli operatori temporali vincolati nel tempo (es. $\diamond_{[a,b]}$) vengono trasformati in operatori LTL standard combinati con predicati aritmetici che gestiscono gli intervalli di tempo (tramite un indice di contatore $j$ e un indice di inizio $j_0$).
• Strumento: La traduzione permette di utilizzare il model checker SPIN. SPIN esplora lo spazio degli stati del sistema (modellato in Promela con codice C incorporato per la dinamica continua) e verifica le proprietà LTLP.
• Gestione dei dati: I segnali reali vengono discretizzati in interi (es. moltiplicando per 1000) per garantire che lo spazio degli stati rimanga finito, rendendo il problema decidibile.

3. Contributi Chiave

1. Introduzione di SSTL: La prima astrazione sincrona (discreta) della STL che permette la verifica statica decidibile sia per proprietà di sicurezza che di vivacità.
2. Formalizzazione Teorica: Definizione formale della sintassi, semantica e dimostrazione che l'Ipotesi di Invarianza del Segnale (SIH) è una condizione necessaria e sufficiente per l'equivalenza tra STL e SSTL.
3. Metodo di Traduzione Decidibile: Un algoritmo di traduzione da SSTL a LTLP che permette l'uso di strumenti di verifica esistenti (SPIN) per sistemi CPS complessi.
4. Validazione su Casi Reali: Applicazione e verifica di un modello cardiaco umano a 33 nodi, dimostrando la capacità di rilevare difetti in modelli sani e patologici.

4. Risultati Sperimentali

Gli autori hanno valutato il framework su tre casi di studio di crescente complessità:

1. Controllore di Semaforo: Verifica di proprietà di sicurezza (mutua esclusione) e vivacità. Il sistema ha identificato correttamente una violazione di una proprietà di equità (fairness).
2. Attraversamento Pedonale: Sistema con segnali interi. Ha verificato con successo proprietà di sicurezza (assenza di conflitti) e limiti di coda, identificando rapidamente violazioni in modelli difettosi.
3. Modello Cardiaco (33 nodi):
   • Modello Sano: Tutte le proprietà critiche (conduzione atrio-ventricolare, periodo refrattario, vivacità) sono state verificate come soddisfatte.
   • Modelli Patologici: Introducendo blocchi di conduzione (AV, LBB, RBB), la proprietà di sicurezza relativa ai tempi di conduzione AV ($\varphi_{AV}$) è risultata violata, mentre le proprietà di vivacità sono rimaste soddisfatte.
   • Prestazioni: I tempi di verifica sono variati da pochi secondi a circa 66 secondi per le proprietà più complesse, con un uso della memoria che ha raggiunto i 9 GB per il modello cardiaco (gestibile tramite tecniche di riduzione dello stato).

5. Significato e Impatto

Questo lavoro è significativo perché colma il divario tra la teoria dei sistemi continui e la pratica della verifica formale discreta:

• Decidibilità: Risolve il problema dell'indecidibilità della STL statica, permettendo la verifica completa di sistemi critici prima della distribuzione.
• Completezza: A differenza di approcci precedenti che si limitavano alla sicurezza, SSTL supporta anche le proprietà di vivacità, cruciali per garantire che un sistema non si blocchi.
• Praticità: Sfruttando SPIN e la traduzione in LTLP, offre una soluzione implementabile senza richiedere complessi risolutori SMT o astrazioni di raggiungibilità costose.
• Affidabilità: La dipendenza dalla SIH fornisce un criterio chiaro per determinare quando una verifica discreta è un'astruzione fedele del sistema continuo, rendendo il processo di verifica rigoroso e matematicamente fondato.

In sintesi, SSTL fornisce un ponte teorico e pratico per la prossima generazione di sistemi cyber-fisici autonomi e sicuri, permettendo la verifica formale di proprietà temporali complesse in ambienti reali.