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.

翻译：随机信息物理系统（CPS）已渗透至关键基础设施，从自动驾驶汽车到医疗设备。然而，尽管理论奠基已近十年，针对此类系统中概率动态特性进行运行时验证的工具仍普遍缺失。本文提出SENTIL，一种新颖的运行时验证工具，可为表示为概率信号时序逻辑（PrSTL）的规约提供具有可证明统计保证的运行时监控。SENTIL将高效的Rust核心与通用生态系统集成相结合，在提供通过统计模型检验、序贯概率比检验和自适应稀有事件估计实现的严格概率保证的同时，性能超越现有确定性监控器。SENTIL采用增量鲁棒性计算的流式算法、并行蒙特卡洛采样，以及语言无关的C-ABI接口，支持无缝部署于ROS、Apollo、MATLAB Simulink和AUTOSAR平台，并可直接集成至C、C++、Python和Java语言。为验证所提工具的有效性，我们分别在自动驾驶车辆监控、医疗设备验证及生物网络等场景下进行测试，结果表明SENTIL在保持可证明置信区间的前提下，性能较现有工具提升10-1000倍。SENTIL为开源工具(https://github.com/sedislab/SENTIL)，其将概率运行时验证定位为所有真实世界安全关键随机系统的可部署基础设施。