Runtime Verification of Stochastic, Faulty Systems

We desire a capability for the lifelong verification of complex embedded systems that degrade over time, such as a semi-autonomous car. The field of runtime verification has developed many tools for monitoring the safety of software systems in real time. However, these tools do not allow for uncertainty in the system’s state or failure, both of which are essential for monitoring hardware as it degrades. This work augments runtime verification with techniques from model-based estimation in order to provide a capability for monitoring the safety criteria of mixed hardware/software systems that is robust to uncertainty and hardware failure.

We begin by framing the problem as runtime verification of stochastic, faulty, hidden-state systems. We solve this problem by performing belief state estimation over the combined state of the Büchi automata representing the safety requirements and the probabilistic hierarchical constraint automata representing the embedded system. This method provides a clean framing of safety monitoring of mixed stochastic systems as an instance of Bayesian filtering.