Data-driven and Model-based Verification: a Bayesian Identification Approach
For engineers verifying safety-critical systems with uncertain dynamics, this provides a principled method to quantify verification confidence.
This work develops a Bayesian identification approach for formal verification of systems with partly unknown dynamics, computing confidence that a system satisfies temporal logic properties under noisy measurements. In a case study on a partly unknown linear system, the method successfully verifies bounded- and unbounded-time safety.
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.