AI 中文总结
本文针对CPS规范，提出信号-频谱时序逻辑（S2TL），对比发现其比时域规范更适用于线性插值轨迹，且噪声容忍度更优，保真度相当。
AI 中文摘要
规范语言对网络物理系统（CPS）的验证与确认至关重要。大多数最先进的规范语言采用信号的时域表示，但其并不总能适用于描述信号形状与动态行为。相反，控制与机器人学等领域使用频域表示来刻画这些行为。时频表示结合了两个领域的能力，本文研究将时频表示用于指定CPS需求。本文分析了现有的CPS需求分类，以确定哪些需求类别可从时频表示中受益；推导了采用时频表示的规范语言的必要条件，并提出了信号-频谱时序逻辑（S2TL），该语言支持对频率区间及频率分量间关系的断言。本文将S2TL语义运用于监控CPS轨迹，并实现了一个监控器；为已识别的需求类别定义了规范模板，从适用性、表达保真度与监控的噪声容忍度三个方面比较了时域与时频域的公式化表示。研究发现，时域规范仅适用于包含阶跃式变化或使用常数插值的输入轨迹，而时频规范可将评估扩展至通过线性插值生成的轨迹，且提升了对偏移量与高频噪声的容忍度，同时对预期系统属性的保真度相当。
英文摘要
Specification languages are instrumental to the Verification \& Validation of Cyber-Physical Systems (CPSs). Most state-of-the-art specification languages use the time-domain representation of signals, which is not always suitable for describing signal shapes and dynamic behaviours. Instead, fields like control and robotics use the frequency-domain representation to characterise these behaviours. Time-frequency representations combine the capabilities of both domains. We investigate the use of time-frequency representations to specify CPS requirements. We analyse existing taxonomies of CPS requirements to identify which requirement classes can benefit from time-frequency representations. We derive the desiderata for a specification language that uses time-frequency representations and propose Signal-Spectrum Temporal Logic (S2TL), a language enabling assertions over frequency intervals and relations between frequency components. We operationalise the S2TL semantics for monitoring CPS traces, and implement a monitor. We define specification templates for the identified requirement classes and compare time- and time-frequency-domain formulations in terms of applicability, expression fidelity, and noise tolerance of monitoring. We observe that, while time-domain specifications are applicable only to input traces containing step-like changes or using constant interpolation, time-frequency specifications extend their evaluation to traces generated through linear interpolation, and improve tolerance to offset and high-frequency noise, while achieving comparable fidelity to the intended system properties.
