Monitoring the correctness of distributed cyber-physical systems is essential. Detecting possible safety violations can be hard when some samples are uncertain or missing. We monitor here black-box cyber-physical system, with logs being uncertain both in the state and timestamp dimensions: that is, not only the logged value is known with some uncertainty, but the time at which the log was made is uncertain too. In addition, we make use of an over-approximated yet expressive model, given by a non-linear extension of dynamical systems. Given an offline log, our approach is able to monitor the log against safety specifications with a limited number of false alarms. As a second contribution, we show that our approach can be used online to minimize the number of sample triggers, with the aim at energetic efficiency. We apply our approach to three benchmarks, an anesthesia model, an adaptive cruise controller and an aircraft orbiting system.
翻译:监控分布式信息物理系统的正确性至关重要。当某些样本存在不确定性或缺失时,检测潜在的安全违规可能变得困难。本文监控黑盒信息物理系统,其日志在状态和时间戳两个维度上均存在不确定性:即不仅记录的数值存在不确定性,日志生成的时间也是不确定的。此外,我们利用一种过近似但富有表现力的模型,该模型由动力系统的非线性扩展给出。针对离线日志,我们的方法能够在安全规范约束下以有限的误报率完成监控。作为第二项贡献,我们证明该方法可用于在线场景中以最小化样本触发次数,从而实现节能目标。我们将该方法应用于三个基准测试:麻醉模型、自适应巡航控制器和飞机轨道系统。