Signal temporal logic (STL) is widely used to specify and analyze properties of cyber-physical systems with continuous behaviors. But STL model checking is still quite limited; existing STL model checking methods are either incomplete or very inefficient. This paper presents a new SMT-based model checking algorithm for verifying STL properties of cyber-physical systems. We propose a novel technique to reduce the STL bounded model checking problem to the satisfiability of a first-order logic formula over reals, which can be solved using state-of-the-art SMT solvers. Our algorithm is based on a new theoretical result, presented in this paper, to build a small but complete discretization of continuous signals, which preserves the bounded satisfiability of STL. Our modular translation method allows an efficient STL model checking algorithm that is refutationally complete for bounded signals, and that is much more scalable than the previous refutationally complete algorithm.
Wed 17 NovDisplayed time zone: Hobart change
08:00 - 09:00
|Distribution Models for Falsification and Verification of DNNs|
Felipe Toledo , David Shriver University of Virginia, Sebastian Elbaum University of Virginia, Matthew B Dwyer University of VirginiaPre-print
|SATune: A Study-Driven Auto-Tuning Approach for Configurable Software Verification Tools|
|Efficient SMT-Based Model Checking for Signal Temporal Logic|