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

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

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.