Many Cyber Physical System (CPS) work in a safety-critical environment, where correct execution, reliability and trustworthiness are essential. Signal Temporal Logic (STL) provides a formal framework for checking safety-critical CPS. However, static verification of STL is undecidable in general, except when we want to verify using run-time-based methods, which have limitations. We propose Synchronous Signal Temporal Logic (SSTL), a decidable fragment of STL, which admits static safety and liveness property verification. In SSTL, we assume that a signal is sampled at fixed discrete steps, called ticks, and then propose a hypothesis, called the Signal Invariance Hypothesis (SIH), which is inspired by a similar hypothesis for synchronous programs. We define the syntax and semantics of SSTL and show that SIH is a necessary and sufficient condition for equivalence between an STL formula and its SSTL counterpart. By translating SSTL to LTL_P (LTL defined over predicates), we enable decidable model checking using the SPIN model checker. We demonstrate the approach on a 33-node human heart model and other case studies.

翻译：许多信息物理系统（CPS）运行在安全关键环境中，其正确执行、可靠性与可信性至关重要。信号时序逻辑（STL）为检验安全关键的信息物理系统提供了形式化框架。然而，除基于运行时的方法（此类方法存在局限性）外，STL的静态验证通常是不可判定的。本文提出同步信号时序逻辑（SSTL）——STL的一个可判定子集，允许进行安全性与活性属性的静态验证。在SSTL中，我们假设信号在固定的离散步长（称为滴答）上被采样，并据此提出一个假设，即信号不变性假设（SIH），其灵感来源于同步程序的相似假设。我们定义了SSTL的语法与语义，并证明SIH是STL公式与其SSTL对应公式之间等价的充要条件。通过将SSTL转化为基于谓词的LTL，即LTL_P，我们能够利用SPIN模型检验器实现可判定的模型检验。我们在一个33节点的人体心脏模型及其他案例研究中展示了该方法。