Jakšić Stefan, Bartocci Ezio, Grosu Radu, Nguyen Thang, Ničković Dejan
1Austrian Institute of Technology, Donau-City-Straße 1, Vienna, Austria.
2Faculty of Informatics, TU Wien, Treitlstraße 3, Vienna, Austria.
Form Methods Syst Des. 2018;53(1):83-112. doi: 10.1007/s10703-018-0319-x. Epub 2018 Mar 27.
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 , 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.
在网络物理系统（CPS）中，物理行为通常由数字硬件控制。因此，连续行为在处理之前会通过采样和量化进行离散化。量化CPS行为与其规范之间的相似性是评估此类系统正确性和质量的重要因素。我们提出了一种用于测量数字化CPS信号与信号时序逻辑（STL）规范之间鲁棒性的新方法。我们首先基于 为STL配备定量语义，这是一种量化数字化CPS行为之间空间和时间不匹配的度量。然后，我们开发了一种动态规划算法，用于计算数字化信号与STL规范之间的鲁棒度。为了推广基于硬件的监视器，我们在FPGA中实现了我们的方法。我们在研究社区定义的汽车基准测试以及从现代汽车中使用的磁传感器获得的实际数据上对其进行了评估。
