Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems

Partha Roop, Sobhan Chatterjee, Avinash Malik, Nathan Allen, Logan Kenwright

Abstract

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.

Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems

Abstract

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.

Paper Structure

This paper contains 27 sections, 4 theorems, 32 equations, 3 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. Heart Model Case Study
  4. STL Specification for Heart Model
  5. Property 1: Atrioventricular Conduction Safety
  6. Property 2: Ventricular Refractory Period
  7. Property 3: Liveness Property
  8. Challenges with STL
  9. Synchronous Signal Temporal Logic (SSTL)
  10. Verification of SSTL properties
  11. LTL with predicates
  12. SSTL to LTL translation
  13. Nesting of Formulas
  14. SSTL verification procedure
  15. SPIN support for LTL$_{\mathcal{P}}$
  16. ...and 12 more sections

Key Result

theorem 1

If a trace $w$Please see Appendix appendix:syntax_and_semantics_of_stl for the definition of STL trace, syntax and semantics. contains signals that satisfy the SIH and the trace also satisfies the STL formula $\varphi$, then for any $t \in \mathbb{R}_{\geq0}$ and $[t] \in \mathbb{N}_{\geq0}$, we hav The proof of this theorem is provided in the Appendix appendix:stl_to_sstl_satisfaction.

Figures (3)

  • Figure 1: The 33-node heart model. (Adapted from yip2018towards)
  • Figure 2: Comparison of STL and SSTL for the heart model scenario.
  • Figure 3: Illustration of the mapping between the continuous time and the discrete time assuming that the signal is sampled at a fixed interval $\Delta t = 0.5$ seconds

Theorems & Definitions (23)

  • definition 1
  • definition 2
  • definition 3
  • Remark 1
  • definition 4
  • definition 5
  • theorem 1
  • definition 6
  • definition 7
  • definition 8
  • ...and 13 more