Runtime Verification of Spatio-Temporal Specification Language

MOBILE NETWORKS & APPLICATIONS(2021)

引用 2|浏览17
暂无评分
摘要
Combining spatial and temporal primitives together is quite useful to specify dynamic behaviors of cyber-physical systems. The ability to represent spatio-temporal properties by means of formulas in spatio-temporal logics has recently found important applications in various fields, such as runtime verification, parameter synthesis, and falsification. In this paper, we present a spatio-temporal specification language, STSL , by combining signal temporal logic ( STL ) with a spatial logic 𝒮4_u to characterize spatio-temporal dynamic behaviors of cyber-physical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatio-temporal traces over real-valued signals in dense time, and Boolean signals, by constraining values of spatial objects across threshold predicates. STSL combines the power of temporal modalities and spatial operators and enjoys important properties such as safety and liveness. We provide the falsification problem through extending Lemire’s algorithm and a parameter synthesis procedure by calling the simulated annealing algorithm. We demonstrate the proposed approach on the adaptive cruise control system and path planning of quadrotors.
更多
查看译文
关键词
Spatio-temporal specification language, Falsification, Parameter synthesis, Adaptive cruise control system, Path planning of quadrotors
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要