Validation of stochastic hybrid digital twins

This thesis presents a comprehensive validation and verification framework for Stochastic Hybrid Automata (SHA) models of an industrial decanter centrifuge, building upon previous work that developed SHA-based digital twins using data from GR3N. While the foundational thesis demonstrated the feasibility of learning SHA models for bearing temperature estimation, this work addresses the critical question: are these learned models reliable enough for industrial deployment? The research employs a dual approach combining formal verification and empirical valida tion. Formal verification utilizes UPPAAL’s Statistical Model Checking (SMC) engine to verify that learned SHA models execute correctly, maintain temporal consistency, and satisfy bounded operational constraints. Empirical validation compares simulated bearing temperature trajectories against real sensor measurements across 17 operational traces, quantifying model accuracy through statistical metrics and visual analysis. Results demonstrate that learned SHA models capture bearing thermal behavior during stable operational phases, achieving temperature predictions within quantifiable confidence intervals. However, validation reveals performance degradation during rapid state transi tions, highlighting practical limitations for predictive maintenance applications. Statistical analysis across multiple traces provides objective metrics for model reliability assessment. Key contributions include an integrated verification and validation framework combining formal methods with empirical testing, robust preprocessing pipelines handling real-world data inconsistencies, full-trace validation methodology ensuring comprehensive model assessment. This work establishes methodological foundations for deploying data-driven hybrid models in Industry 4.0 predictive maintenance systems with measurable confidence in their reliability.

Questa tesi presenta un framework completo di validazione e verifica per modelli di automi ibridi stocastici (SHA) di una centrifuga decanter industriale, basandosi su lavori precedenti che hanno sviluppato gemelli digitali basati su SHA utilizzando i dati di GR3N. Mentre la tesi di base ha dimostrato la fattibilità dell’apprendimento di modelli SHA per la stima della temperatura dei cuscinetti, questo lavoro affronta la domanda critica: questi modelli appresi sono sufficientemente affidabili per l’impiego industriale? La ricerca impiega un duplice approccio che combina verifica formale e validazione empirica. La verifica formale utilizza il motore di Statistical Model Checking (SMC) di UPPAAL per verificare che i modelli SHA appresi vengano eseguiti correttamente, mantengano la coerenza temporale e soddisfino vincoli operativi limitati. La validazione empirica confronta le traiettorie simulate della temperatura dei cuscinetti con le misurazioni reali dei sensori su 17 tracce operative, quantificando l’accuratezza del modello attraverso metriche statistiche e analisi visiva. I risultati dimostrano che i modelli SHA appresi catturano il comportamento termico dei cuscinetti durante le fasi operative stabili, ottenendo previsioni di temperatura entro intervalli di confidenza quantificabili. Tuttavia, la convalida rivela un degrado delle prestazioni durante rapide transizioni di stato, evidenziando i limiti pratici delle applicazioni di manutenzione predittiva. L’analisi statistica su più tracce fornisce metriche oggettive per la valutazione dell’affidabilità del modello. I contributi chiave includono un framework integrato di verifica e convalida che combina metodi formali con test empirici, robuste pipeline di pre-elaborazione che gestiscono le incoerenze dei dati reali e una metodologia di convalida full-trace che garantisce una valutazione completa del modello. Questo lavoro stabilisce le basi metodologiche per l’implementazione di modelli ibridi basati sui dati nei sistemi di manutenzione predittiva dell’Industria 4.0 con una misurabile affidabilità.