SaSTL: Spatial Aggregation Signal Temporal Logic for Runtime Monitoring in Smart Cities
SaSTL: Spatial Aggregation Signal Temporal Logic for Runtime Monitoring in Smart Cities
复制标题
DOI：
10.1109/iccps48487.2020.00013
复制
发表时间：
2019-08
期刊：
影响因子：
--
通讯作者：
Meiyi Ma;E. Bartocci;Eli Lifland;J. Stankovic;Lu Feng
中科院分区：
文献类型：
--
作者：
Meiyi Ma;E. Bartocci;Eli Lifland;J. Stankovic;Lu Feng
我们提出了SaSTL（一种新型空间聚合信号时间逻辑），用于高效运行时监控智能城市的安全和性能要求。我们首先描述了对1,000多个智慧城市需求的研究，其中一些需求无法使用现有的逻辑（如信号时序逻辑（STL）及其变体）来指定。为了解决这一限制，我们开发了两个新的逻辑运算符在SaSTL，以增强STL表达空间聚集和空间计数特性，常见于真实的城市的要求。我们还开发了高效的监控算法，可以在多个数据流上并行检查SaSTL要求（例如，由空间分布在城市中的多个传感器产生）。我们通过应用两个具有大规模真实的城市传感数据的案例研究（例如，在一个需求中多达10，000个传感器）。实验结果表明，SaSTL具有比其他时空逻辑更高的覆盖率表达能力，并显著减少了监控需求的计算时间。我们还通过模拟实验证明了SaSTL监视器可以帮助提高智慧城市的安全性和性能。
We present SaSTL—a novel Spatial Aggregation Signal Temporal Logic—for the efficient runtime monitoring of safety and performance requirements in smart cities. We first describe a study of over 1,000 smart city requirements, some of which can not be specified using existing logic such as Signal Temporal Logic (STL) and its variants. To tackle this limitation, we develop two new logical operators in SaSTL to augment STL for expressing spatial aggregation and spatial counting characteristics that are commonly found in real city requirements. We also develop efficient monitoring algorithms that can check a SaSTL requirement in parallel over multiple data streams (e.g., generated by multiple sensors distributed spatially in a city). We evaluate our SaSTL monitor by applying to two case studies with large-scale real city sensing data (e.g., up to 10,000 sensors in one requirement). The results show that SaSTL has a much higher coverage expressiveness than other spatial-temporal logics, and with a significant reduction of computation time for monitoring requirements. We also demonstrate that the SaSTL monitor can help improve the safety and performance of smart cities via simulated experiments.