SHF: Small: Premonition: A Methodology for Predictive Monitoring with Probabilistic Guarantees

无人驾驶飞行器、医疗设备和自动驾驶汽车等自主系统的设计具有挑战性，因为其固有的软件复杂性以及操作环境的不确定性。 不幸的是，许多这些自主系统也是安全关键的;当这些系统发生故障时，会对人类生命和财产造成真实的悲剧性影响。 长期以来，在这些自主网络物理系统运行时监控其安全性一直被视为确保这些系统安全的可扩展解决方案。这种安全属性通常可以使用诸如信号时序逻辑（STL）的逻辑形式来编写。 该项目开发了一个名为预感的模块化框架，用于监测自主网络物理系统的时间逻辑属性。 预感框架的以下能力突出了其新奇：（1）预测性监控，以在违规实际发生之前预测安全属性的故障;（2）以低内存和感测开销执行的监控的资源感知;以及最后，3）概率保证，以提供对所做预测的准确性的可量化界限。预感框架是高度跨学科的：它将预测时间序列数据未来值的统计方法与正式方法的技术相结合。 创新的关键是在新的技术，以获得概率保证的安全属性是否会被违反的系统在未来。这样的保证是针对不同类型的系统模型获得的。 对于数据驱动的系统模型，Premonition将先前的随机过程预测工作与STL的监控算法结合起来。对于动态系统模型，该框架引入了新的算法来监控STL属性对系统未来可达状态的过度近似。 对于具有显式不确定性模型的系统模型，该框架侧重于资源感知的预测监控。对于具有不可观测状态的系统，它提供了一种新的潜在状态预测监控算法，即通过监控系统的可观测状态，对隐藏的系统状态在未来是否违反给定性质给出概率保证的算法。 概率保证对于设计执行和警告机制以提供系统的安全保证是有用的。该项目的影响是为自动胰岛素输送系统、无人机和自动驾驶汽车等自动系统提供动态安全保证案例。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Autonomous systems such as unmanned aerial vehicles, medical devices and self-driving cars are challenging to design because of the inherent software complexity, as well as uncertainty in their operating environment. Unfortunately, many of these autonomous systems are also safety-critical; there are real tragic implications on human life and property when these systems malfunction. Monitoring the safety of such autonomous cyber-physical system while they are operating has long been viewed as scalable solution to ensure safety of these systems. Such safety properties can often be written using logical formalisms such as Signal Temporal Logic (STL). The project develops a modular framework called Premonition for monitoring temporal-logic properties of autonomous cyber-physical systems. The following abilities of Premonition framework highlight its novelty: (1) Predictive monitoring to forecast the failure of a safety property before a violation actually occurs; (2) Resource-awareness for monitoring that is performed with low memory and sensing overhead; and finally, 3) Probabilistic guarantees for providing quantifiable bounds on the accuracy of the predictions made.The Premonition framework is highly interdisciplinary: it combines statistical methods for predicting future values of time-series data with techniques from formal methods. The key site for innovation is in new techniques for obtaining probabilistic guarantees on whether a safety property will be violated by the system in the future. Such guarantees are obtained for different kinds of system models. For data-driven system models, Premonition weaves prior work on forecasting for stochastic processes with monitoring algorithms for STL. For dynamical system models, the framework introduces new algorithms to monitor STL properties on over-approximations of future reachable states of the system. For system models with explicit uncertainty models, the framework focuses on resource-aware predictive monitoring. For systems with unobservable states, it provides new algorithms for latent- xstate predictive monitoring, i.e. algorithms that give probabilistic guarantees on whether the hidden system states violate a given property in the future, by monitoring the observable states of the system. Probabilistic guarantees are useful for designing enforcement and warning mechanisms to provide safety assurance for systems. This project's impacts are in making dynamic safety-assurance cases for autonomous systems such as automated insulin-delivery systems, unmanned aerial vehicles and self-driving cars.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.