10.1007/978-3-030-88494-9_1
10.1007/978-3-030-88494-9_1
复制标题
10.1007/978-3-030-88494-9_1
DOI：
10.1007/978-3-030-88494-9_1
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Anik Momtaz, Niraj Basnet
中科院分区：
文献类型：
--
作者：
Anik Momtaz, Niraj Basnet
本文解决了网络物理系统（CPS）中分布连续时间和连续值信号的谓词违例检测问题。我们假设一个部分同步设置，其中时钟同步算法保证所有信号之间的时钟漂移的界限。我们引入了一种新的重新计时方法，该方法允许在不共享全局时间视图的连续时间信号中对谓词的正确性进行推理。将生成的问题编码为SMT问题，并引入有效解决SMT编码的技术。利用简单的物理动力学知识可以进一步减少运行时间。我们在两个分布式CPS应用中完全实现了我们的方法：监测自主地面车辆网络和空中车辆网络。结果表明，在某些情况下，甚至可以足够快地监控分布式CPS，以便在自动驾驶车队上进行在线部署。
This paper solves the problem of detecting violations of predicates over distributed continuous-time and continuous-valued signals in cyber-physical systems (CPS). We assume a partially synchronous setting, where a clock synchronization algorithm guarantees a bound on clock drifts among all signals. We introduce a novel retiming method that allows reasoning about the correctness of predicates among continuoustime signals that do not share a global view of time. The resulting problem is encoded as an SMT problem and we introduce techniques to solve the SMT encoding efficiently. Leveraging simple knowledge of physical dynamics allows further runtime reductions. We fully implement our approach on two distributed CPS applications: monitoring of a network of autonomous ground vehicles, and a network of aerial vehicles. The results show that in some cases, it is even possible to monitor a distributed CPS sufficiently fast for online deployment on fleets of autonomous vehicles.