SENTIL: A Runtime Verification Tool for Probabilistic Temporal Logic

TL;DR

SENTIL is a new runtime verification tool for stochastic cyber-physical systems that offers high performance and probabilistic guarantees, enabling deployment across various safety-critical applications.

Contribution

It introduces SENTIL, a novel probabilistic runtime verification tool with efficient algorithms, broad platform support, and proven effectiveness in real-world scenarios.

Findings

Achieves 10-1,000× performance improvements over existing tools.

Provides rigorous probabilistic guarantees through statistical model checking.

Successfully validated across autonomous vehicles, medical devices, and biological networks.

Abstract

Stochastic cyber-physical systems (CPS) permeate critical infrastructure, from autonomous vehicles to medical devices. Yet, tools for runtime verification of such systems capturing the probabilistic dynamics in stochastic systems remain generally absent despite theoretical foundations established nearly a decade ago. In this paper, we present SENTIL, a novel runtime verification tool with provable statistical guarantees for the runtime monitoring of requirements expressed as Probabilistic Signal Temporal Logic (PrSTL). SENTIL combines an efficient Rust core with universal ecosystem integration, delivering performance exceeding existing deterministic monitors while providing rigorous probabilistic guarantees through statistical model checking, sequential probability ratio testing, and adaptive rare event estimation. SENTIL employs streaming algorithms for incremental robustness computation, parallel Monte Carlo sampling, and a language-agnostic C-ABI enabling seamless deployment across ROS, Apollo, MATLAB Simulink, and AUTOSAR platforms, and direct integration in C, C++, Python, and Java. To validate the effectiveness of the proposed tool, we validate SENTIL across various scenarios spanning autonomous vehicle monitoring, medical device validation, and biological networks, demonstrating 10-1,000$\times$ performance improvements over existing tools while maintaining provable confidence intervals. SENTIL is open source (\href{https://github.com/sedislab/SENTIL}{\texttt{sedislab/SENTIL}}) and it positions probabilistic runtime verification as a deployable infrastructure for all real-world safety-critical stochastic systems.