Quantitative monitoring of STL with edit distance
Quantitative monitoring of STL with edit distance
复制标题
DOI：
10.1007/s10703-018-0319-x
复制
发表时间：
2018-08-01
影响因子：
0.8
通讯作者：
Nickovic, Dejan
中科院分区：
文献类型：
--
作者：
Jaksic, Stefan;Bartocci, Ezio;Nickovic, Dejan
在网络物理系统（CPS）中，物理行为通常由数字硬件控制。结果，连续行为在处理之前通过采样和量化被离散。量化CPS行为及其规范之间的相似性是评估此类系统的正确性和质量的重要组成部分。我们提出了一个新的程序，用于测量数字化CPS信号和信号时间逻辑（STL）规范之间的鲁棒性。我们首先根据加权编辑距离为STL配备定量语义，该指标量化了数字化CPS行为之间的空间和时间不匹配。然后，我们开发了一种动态编程算法，用于计算数字化信号和STL规范之间的鲁棒性度。为了促进基于硬件的显示器，我们在FPGA中实施了方法。我们对研究社区定义的汽车基准以及从现代汽车中使用的磁性传感器获得的现实数据进行了评估。
In cyber-physical systems (CPS), physical behaviors are typically controlled by digital hardware. As a consequence, continuous behaviors are discretized by sampling and quantization prior to their processing. Quantifying the similarity between CPS behaviors and their specification is an important ingredient in evaluating correctness and quality of such systems. We propose a novel procedure for measuring robustness between digitized CPS signals and signal temporal logic (STL) specifications. We first equip STL with quantitative semantics based on the weighted edit distance, a metric that quantifies both space and time mismatches between digitized CPS behaviors. We then develop a dynamic programming algorithm for computing the robustness degree between digitized signals and STL specifications. In order to promote hardware-based monitors we implemented our approach in FPGA. We evaluated it on automotive benchmarks defined by research community, and also on realistic data obtained from magnetic sensor used in modern cars.