Data-driven and Model-based Verification: a Bayesian Identification Approach

TL;DR

This paper introduces a Bayesian inference-based verification method combining measurement data and models to assess system safety properties, especially for systems with partially unknown dynamics, using reachability analysis.

Contribution

It presents a novel formal verification approach that integrates Bayesian inference with reachability analysis for systems with uncertain dynamics.

Findings

Successfully applied to a linear time-invariant system

Provides confidence levels for safety verification

Addresses both bounded and unbounded time properties

Abstract

This work develops a measurement-driven and model-based formal verification approach, applicable to systems with partly unknown dynamics. We provide a principled method, grounded on reachability analysis and on Bayesian inference, to compute the confidence that a physical system driven by external inputs and accessed under noisy measurements, verifies a temporal logic property. A case study is discussed, where we investigate the bounded- and unbounded-time safety of a partly unknown linear time invariant system.