Sintesi Tecnica: Un Framework Unificato per la Verifica a Runtime e la Diagnosi Basata su Modelli in Lola

Problematica

I sistemi critici per la sicurezza richiedono non solo il rilevamento dei guasti, ma anche la localizzazione delle loro cause radice per consentire una mitigazione efficace. Mentre la Verifica a Runtime (RV) è efficace nel rilevare deviazioni dal comportamento specificato durante l'esecuzione, e la Diagnosi Basata su Modelli (MBD) è un framework rigoroso per identificare componenti difettosi, queste due tecniche hanno storicamente operato in isolamento. I monitor RV tradizionali analizzano il comportamento del sistema su sequenze di stati potenzialmente illimitate per rilevare violazioni, mentre la MBD opera tipicamente in un singolo punto temporale non specificato dopo che un guasto è stato rilevato. Inoltre, le integrazioni esistenti spesso non riescono a mappare direttamente le azioni di guasto rilevate ai componenti anormali nel senso della MBD o mancano della capacità di gestire input incerti e dinamiche di guasto temporali all'interno di un framework di ragionamento unificato basato su stream.

Metodologia

Il paper propone un framework unificato che integra la RV basata su stream e la MBD all'interno di Lola, un linguaggio di specifica sincrono basato su stream. La metodologia centrale prevede la codifica sia della verifica che delle informazioni diagnostiche come stream specializzati, consentendo l'osservazione continua e il ragionamento simbolico sotto incertezza.

1. Codifica Unificata in Lola

Gli autori mappano un sistema diagnosticato $S = (sd, comps)$ in un Sistema Lola $(\phi, comps)$:

• Descrizione del Sistema ($sd$): Codificata nello stream di assunzione ($\alpha$), che è vera per definizione. Questo stream contiene la conoscenza comportamentale (ad es. $\neg ab(c) \to beh_c$) e la conoscenza generale del sistema.
• Componenti ($comps$): Ogni componente $c$ è rappresentata da uno stream Booleano interno dove true indica che il componente è anormale ($ab(c)$).
• Osservazioni: Le variabili osservabili del sistema (input/output) sono modellate come stream di input, che possono essere certi (deterministici) o incerti (intervalli o insiemi non deterministici).
• Variabili Non Osservabili: I valori interni del sistema non misurati direttamente sono modellati come stream interni.
• Istanza del Problema di Diagnosi (DPI): Una tupla $(\phi, comps, \Psi)$, dove $\Psi$ rappresenta la cronologia dei vincoli di input fino al tempo corrente.

2. Ragionamento Simbolico e Computazione della Diagnosi

Il framework utilizza un monitor simbolico che mantiene un insieme di vincoli $[\phi]_{\Psi}^{\leq t}$ rappresentante tutti i possibili comportamenti di sistema coerenti con le osservazioni fino al tempo $t$.

• Risoluzione dei Vincoli: Un solver SMT (ad es. Z3) viene utilizzato per verificare la coerenza e derivare implicazioni.
• Derivazione della Diagnosi: Una diagnosi è un'assunzione sullo stato (normale/anormale) dei componenti che rende la descrizione del sistema coerente con le osservazioni. Il framework calcola le diagnosi minime identificando i conflitti minimi (insiemi di componenti che non possono essere tutti normali) e calcolando i loro insiemi di copertura minimi (minimal hitting sets).
• Pruning (Potatura): Per garantire un monitoraggio a tempo costante e spazio costante, le strategie di pruning riscrivono i vincoli per limitare la dimensione dell'insieme dei vincoli, mantenendo solo le informazioni storiche necessarie.

3. Scenari Diagnostici

Il framework supporta tre distinti modi diagnostici basati sulla natura temporale dei guasti dei componenti:

• Diagnosi Multi-Istante: Assume che gli stati dei componenti siano statici su una finestra di $k$ istanti passati ($t-k$ a $t$). Una diagnosi a $k$-istanti spiega tutte le osservazioni all'interno di questa finestra. Il paper dimostra che per specifiche atemporali, le diagnosi a $k$-istanti sono equivalenti all'aggregazione di diagnosi a singolo istante, ma per specifiche temporali (con offset non nulli), forniscono risultati più mirati.
• Diagnosi Temporale: Permette agli stati dei componenti di cambiare nel tempo. Una diagnosi $k$-temporale è un insieme di coppie $(c, t')$ che indica che il componente $c$ è anormale specificamente al tempo $t'$. Questo è critico per identificare guasti transitori (ad es. surriscaldamento) o guasti che si manifestano successivamente a causa della propagazione.
• Impostazioni Estese: Il framework incorpora naturalmente la conoscenza di base (che forza i componenti a essere normali), modelli di guasto forti (specificando comportamenti difettosi specifici) e la modellazione astratta.

Contributi Chiave

1. Codifica Unificata: Un metodo per esprimere le descrizioni di sistema e le assunzioni diagnostiche come stream specializzati in Lola, rappresentando implicitamente tutte le diagnosi valide per il comportamento osservato.
2. Teoria della Diagnosi Multi-Istante: Una teoria generalizzata per diagnosticare guasti invarianti nel tempo su una finestra scorrevole di osservazioni, che include la diagnosi standard a singola osservazione come caso speciale.
3. Diagnosi Temporale: Supporto per l'anormalità variabile nel tempo, consentendo l'identificazione di quando si verifica un guasto, non solo di quale componente è difettoso.
4. Scenari Diagnostici Flessibili: La capacità di gestire elegantemente la conoscenza di base, la modellazione astratta e vari tipi di guasto (persistenti vs transitori) all'interno di un unico framework basato su stream.
5. Implementazione e Valutazione: Un prototipo di implementazione che integra l'algoritmo HS-Tree, QuickXplain e Z3, validato sui benchmark ISCAS85 e ISCAS89.

Risultati

Gli autori hanno valutato il framework su due circuiti Booleani:

• c17 (ISCAS85): Un circuito puramente combinatorio con 6 componenti.
• s27 (ISCAS89): Un circuito sequenziale con 14 componenti.

Risultati:

• Fattibilità: Il framework ha identificato con successo i guasti effettivamente iniettati (stuck-at-false) in entrambi i circuiti.
• Accuratezza Temporale: Per il circuito sequenziale (s27), il framework ha localizzato correttamente i guasti solo quando la finestra di osservazione ($k$) era sufficientemente grande da coprire l'origine del guasto e il tempo di propagazione.
• Performance:
  • Il tempo di esecuzione aumentava con valori di $k$ più grandi. Per c17, la diagnosi a $k$-istante richiedeva fino a 246 ms ($k=0$) e 775 ms ($k=31$) per istante.
  • La diagnosi temporale era significativamente più costosa a causa dell'esplosione combinatoria del trattare $(c, t')$ come componenti distinti. Per c17, la diagnosi temporale richiedeva fino a 8,7 secondi per istante per $k=5$ e 136 secondi per $k=12$.
  • Nonostante il costo computazionale, gli autori notano che con un $k$ costante, i tempi di esecuzione rimanevano indipendenti dalla lunghezza totale della traccia, confermando la viabilità delle strategie di pruning.

Significato e Rivendicazioni

Il paper sostiene di fornire un'integrazione compatta e ben fondata tra la Verifica a Runtime e la Diagnosi Basata su Modelli. La sua importanza risiede nel colmare il divario tra il rilevamento automatico dei guasti (RV) e la localizzazione sistematica dei guasti (MBD) all'interno di un unico framework basato su stream.

Gli autori sottolineano che questo approccio:

• Supporta input incerti e assunzioni ambientali, consentendo un'inferenza raffinata basata sulla conoscenza esperta.
• Abilita la diagnosi online sfruttando il ragionamento simbolico per produrre verdetto ad ogni punto temporale.
• Offre una combinazione sinergica dove i punti di forza della RV (monitoraggio efficiente e continuo) e della MBD (analisi rigorosa della causa radice) sono unificati.
• Fornisce un framework solido dove il monitor simbolico assicura che i valori dedotti siano coerenti con tutti i mondi possibili definiti dai vincoli.

Il lavoro è presentato come una prova di concetto che dimostra la fattibilità dell'uso di Lola per compiti diagnostici complessi, offrendo una base teorica per future applicazioni pratiche in sistemi critici per la sicurezza.