Paper Info
Title
STSL: A Novel Spatio-Temporal Specification Language for Cyber-Physical Systems
Abstract
Combining spatial and temporal primitives together is quite useful to specify dynamic behaviors of cyber-physical systems. The ability to represent spatiotemporal properties by means of formulas in spatiotemporal logics has recently found important applications in various fields, such as runtime verification, parameter synthesis, contract-Based design. In this paper, we present a spatiotemporal specification language, STSL, by combining Signal Temporal Logic (STL) with a spatial logic $\mathcal{S}{4_u}$, to characterize spatiotemporal dynamic behaviors of cyber-physical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatiotemporal 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 approaches on adaptive cruise control system and path planning of quadrotors.
Year
DOI
Venue
2020
10.1109/QRS51102.2020.00048
2020 IEEE 20th International Conference on Software Quality, Reliability and Security (QRS)
Keywords
DocType
ISBN
Spatiotemporal Specification Language,Falsification,Parameter Synthesis,Adaptive Cruise Control System,Path Planning of Quadrotors
Conference
978-1-7281-8914-7
Citations 
PageRank 
References 
0
0.34
22
Authors
7
Name
Order
Citations
PageRank
Tengfei Li122.73
Jing Liu269.92
JieXiang Kang311.03
Haiying Sun424.78
Wei Yin511.36
Xiaohong Chen646.55
Hui Wang710.69