提出可判定的信号时序逻辑，实现对复杂系统的安全验证。
Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems
- 基于固定采样周期和信号不变性假设，构造可判定的时序逻辑
- 将SSTL转化为LTL_P后可用SPIN工具进行模型检测
- 适用于心脏等高安全要求的物理系统验证
许多网络物理系统（CPS）在安全关键环境中运行，正确执行、可靠性和可信度至关重要。信号时序逻辑（STL）为检查安全关键型CPS提供了形式化框架，但一般情况下静态验证是不可判定的，而基于运行时的方法又存在局限。本文提出同步信号时序逻辑（SSTL），这是STL的一个可判定片段，支持静态安全性和活性性质验证。在SSTL中，假设信号以固定的离散时间点（称为ticks）进行采样，并引入信号不变性假设（SIH），该假设受到同步程序中类似假设的启发。我们定义了SSTL的语法与语义，并证明：在满足SIH条件下，STL公式与其对应的SSTL版本等价。通过将SSTL翻译为基于谓词的LTL_P（LTL_P），可使用SPIN模型检查器实现可判定的验证。我们在一个33节点的人类心脏模型及其他案例研究中展示了该方法的有效性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。