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.
翻译:我们介绍SastL -- -- 一个新型的空间聚合信号时空逻辑 -- -- 用于高效运行时间监测智能城市的安全和性能要求。我们首先描述对1 000多个智能城市要求的研究,其中一些要求不能使用现有逻辑,如信号时空逻辑(STL)及其变体。为了应对这一限制,我们在SastL开发了两个新的逻辑操作员,以扩大STL,用于表达空间聚合和空间计数特点,这是在真实城市要求中常见的。我们还开发了高效的监测算法,可以检查在多个数据流(例如,在一个城市中空间分布的多个传感器生成的)平行的SatL要求。我们通过应用大规模实际城市感测数据(例如,在一项要求中高达10,000个传感器)进行的两个案例研究来评估我们的SatL监测。结果显示,SastL的覆盖范围比其他空间时空逻辑要高得多,而且监测要求的计算时间也大大缩短。我们还表明,SatL监测器能够帮助通过模拟实验改善智能城市的安全和性能。