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

无人机、医疗设备和自动驾驶汽车等自动驾驶系统的设计具有挑战性，因为它们固有的软件复杂性以及操作环境的不确定性。不幸的是，这些自主系统中的许多也是安全关键的；当这些系统发生故障时，会对人类的生命和财产造成真正悲惨的影响。长期以来，在这种自主的网络物理系统运行时监控它们的安全一直被视为确保这些系统安全的可扩展解决方案。这样的安全属性通常可以使用诸如信号时态逻辑(STL)之类的逻辑形式来编写。该项目开发了一种名为预感的模块化框架，用于监控自主网络物理系统的时间逻辑属性。预感框架的以下能力突出了它的新颖性：(1)预测性监测，在违规实际发生之前预测安全属性的故障；(2)资源感知，以低内存和检测开销执行监测；以及3)概率保证，为预测的准确性提供可量化的界限。预感框架是高度跨学科的：它结合了预测时间序列数据未来值的统计方法和来自正式方法的技术。创新的关键领域是新技术，以获得关于系统未来是否会侵犯安全属性的概率保证。对于不同类型的系统模型，都得到了这样的保证。对于数据驱动的系统模型，预感将随机过程的预测与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.