Skip to content

Robust Bayesian Verification

Summary

  • A novel Bayesian learning framework enabling the runtime verification of autonomous robots performing critical missions in uncertain environments.

  • We consider regular (occurring regularly during system operation) and singular events occurring zero/once (catastrophic failures, completion of difficult one-off tasks).

  • Our BIPP Bayesian estimator (using partial priors) uses prior knowledge and the lack of runtime data to learn expected ranges of rates for singular events

  • Our IPSP Bayesian estimator (using imprecise probability with sets of priors) uses prior knowledge and runtime data to learn expected ranges of rates for regural events

  • The learnt rate ranges instrument interval continuous-time Markov models

  • Quantitative verification on these models enables computing expected intervals for key system properties capturing the parametric uncertainy of the robotic mission

  • The framework is illustrated on a case study for the verification of an offshore wind-turbine inspection and maintenance robotic mission

Framework

Robust Bayesian Verification Framework

Robust Bayesian Verification Framework

Our end-to-end verification framework supports the online computation of bounded intervals of CTMC properties. The framework integrates our BIPP and IPSP Bayesian interval estimators with interval CTMC model checking1.

Monitoring the system under verification enables to observe both the occurrence of regular events, and the lack of singular events during times when such events could have occurred (e.g., a catastrophic failure not happening when the system performs a dangerous operation).

Our online BIPP estimator and IPSP estimator use these observations to calculate expected ranges for the rates of the monitored events, enabling a Model Generator to continually synthesise up-to-date interval CTMCs that model the evolving behaviour of the system.

The interval CTMCs are synthesised from a parametric CTMC model that captures the structural aspects of the system under verification. The synthesised CTMCs are then continually verified by the PRISM-PSY Model Checker2 to compute value intervals for key system properties. These properties range from dependability (e.g., safety, reliability and availability) and performance (e.g., response time and throughput) properties to resource use and system utility.

Finally, changes in the value ranges of these properties may prompt the dynamic reconfiguration of the system by a Controller module responsible for ensuring that the system requirements are satisfied at all times.

  1. Lubos Brim, Milan Ceska, Sven Drazan, and David Safranek. Exploring parameter space of stochastic biochemical systems using quantitative model checking. In Computer Aided Verification (CAV), pages 107–123, 2013. ↩

  2. Milan Ceska, Petr Pilar, Nicola Paoletti, Lubos Brim, and Marta Kwiatkowska. PRISM-PSY: Precise GPU-accelerated parameter synthesis for stochastic systems. In Tools and Algorithms for the Construction and Analysis of Systems, volume 9636 of LNCS, pages 367–384, 2016. ↩