Skip to content

Software Quality

Temporal-logic falsification

Temporal-logic falsification searches for an input signal that drives a system to break a requirement about its behavior over time. The requirement is a temporal property: the temperature never exceeds a limit, the output settles within two seconds of a setpoint change and stays within a band, the brake response begins within a deadline. It is the bug-finding dual of verification: the deliverable is a counterexample, not a proof.

Its targets are control systems — an engine controller, an autopilot — reached only as black boxes: a Simulink/Stateflow model, or a bench rig with nonlinear dynamics and a learned component or two. There is no tractable finite model to model-check, and the space of possible input signals is infinite, so proving the requirement holds is out of reach. Where the Stateflow model is instead white-box and finite, it can be formally verified or have tests generated directly (see state machines).

What it catches

  • Temporal-requirement violations that a point assertion cannot express. Overshoot past a safety envelope, a settling time that misses its deadline, a transient spike that appears only under a specific input ramp. The requirement is a property of the whole trajectory, not of one output value.
  • Counterexamples as concrete, replayable input signals. A falsifying run is an executable witness: the exact stimulus that made the system misbehave, ready to hand to a developer.
  • Failures in black-box and learned components that formal verification cannot enter, because falsification only needs to run the system, not reason about its internals.

Signal temporal logic

The requirement is written in signal temporal logic (STL), introduced for monitoring continuous signals by Maler and Ničković (Maler and Ničković 2004)1. STL combines atomic predicates over real-valued signals (speed < 120) with boolean connectives and time-bounded temporal operators: G[a,b] (always on the interval), F[a,b] (eventually), and U[a,b] (until). An envelope requirement reads G[0,30](speed < 120); a bounded-response requirement reads G(brake → F[0,1](decel > 0.5)). Unlike a plain assertion, STL states properties of behavior across an interval of time, which is what control requirements actually are.

Robustness: the quantitative semantics that makes search work

Boolean satisfaction gives an optimizer nothing to climb: almost every input signal simply satisfies the property, a flat landscape with no gradient. STL's decisive feature is a robustness semantics (Fainekos and Pappas 2009)2: a real number that is positive when the signal satisfies the requirement, with magnitude measuring the margin, and negative when it violates, with magnitude measuring how far into violation. It is defined recursively down the formula, a predicate f(x) > 0 scoring f(x), conjunction becoming min, disjunction max, always an infimum over its interval and eventually a supremum. Donzé and Maler refined it with space and time robustness (Donzé and Maler 2010)3.

Robustness turns falsification into numeric optimization: the search drives the robustness below zero. That makes negative robustness a fitness function and falsification a search-based test-generation problem.

Because the system is a black box and robustness is non-convex and non-smooth, falsification uses derivative-free global optimization over a finite-dimensional parameterization of the input signal (the control points of a piecewise-constant or piecewise-linear input): simulated annealing, CMA-ES, cross-entropy, and, when each simulation is expensive, Bayesian optimization with a surrogate model to spend simulations sparingly.

The recurring difficulty is that robustness can mask its own gradient: the min and inf in a conjunctive, always-quantified requirement let a comfortably-satisfied part hide a nearly-violated one. Alternative smooth or cumulative robustness semantics are an active response to this.

Tools and the benchmark

  • S-TaLiRo (Annpureddy et al. 2011)4 (originally MATLAB, now also a Python port) and Breach (MATLAB, Simulink-focused) are the two established tools; each monitors robustness and drives a falsification search, and Breach also does parameter synthesis.
  • ARIsTEO layers surrogate modeling on S-TaLiRo for costly Simulink plants.
  • Berkeley's VerifAI couples falsification to Scenic scenarios for systems with learned perception.
  • The ARCH-COMP falsification category is an annual friendly competition that benchmarks these tools on shared models (automatic transmission, abstract fuel control, aircraft), the cyber-physical analogue of the verification competitions (Ernst et al. 2021)5.

Where it sits among neighbors

  • The dual of model checking. Model checking proves no violation exists but needs a tractable model; falsification finds a violation and needs only to run the system. Reachability analysis (the over-approximating, abstract-interpretation style) is the sound counterpart that proves safety at the cost of conservatism.
  • Its oracle is a runtime monitor. Computing STL robustness over a trace is used offline inside the search and online as a runtime safety monitor; the Responsibility-Sensitive Safety envelope on the autonomous-systems page is a hand-built instance of exactly this.
  • A sibling of fuzzing and property-based testing. All generate inputs to break a property; falsification's distinctive coordinates are that it generates continuous input signals and its oracle is a quantitative temporal-logic requirement over the resulting trajectory.

When to use, when not

Use:

  • For reactive control and cyber-physical systems whose requirements are temporal (deadlines, settling, envelopes), especially black-box Simulink plants and systems with learned components that formal verification cannot enter.
  • When a concrete failing input is worth more than a proof, which is the usual case during development.
  • With a surrogate-model or Bayesian search when each simulation is expensive.

Don't:

  • As a safety guarantee. No counterexample found is not a proof; pair falsification with reachability analysis or model checking where a guarantee is required.
  • For requirements that are not temporal. A stateless input-output check is a job for example or property-based tests; STL earns its cost when the property is about behavior over time.
  • Without attention to the robustness landscape. A masked or flat robustness defeats a naive optimizer; the specification's shape, and the choice of semantics, decide whether the search converges.

Evidence

  • Robustness semantics make falsification tractable, converting a boolean pass/fail into an objective a black-box optimizer can minimize (Fainekos and Pappas 2009; Donzé and Maler 2010)2 3.
  • The tools falsify real requirements on shared benchmarks, and the ARCH-COMP falsification reports track how reliably, across automotive and aerospace models (Ernst et al. 2021)5. Effectiveness depends heavily on the input parameterization and the robustness landscape rather than being uniform across problems.
  • Scope. Falsification is sound for finding bugs and silent on their absence. It reduces the uncertainty that a temporal requirement is violable; it does not certify that the requirement holds, and it checks only the requirements a person took the trouble to formalize.

Classification

  • Quality dimensions: Functionality (whether the system meets its temporal requirement), Reliability: safety (safety-envelope and robustness requirements that hold over time), Performance (signal temporal logic naturally encodes settling time, overshoot, and response-time bounds).
  • Area: Cyber-physical, control, and hybrid systems with real-time temporal requirements: automotive and aerospace control (Simulink/Stateflow plants), medical devices, robotics, and any reactive system whose specification is about behavior over time.
  • Guarantee: Empirical — a search for a counterexample; a falsifying trace is a real violation, but finding none is not a proof the requirement holds.

Referenced by

References

  1. Maler, Oded, and Dejan Ničković. 2004. "Monitoring Temporal Properties of Continuous Signals." Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems (FORMATS/FTRTFT 2004), 152–66. https://doi.org/10.1007/978-3-540-30206-3_12. ↩

  2. Fainekos, Georgios E., and George J. Pappas. 2009. "Robustness of Temporal Logic Specifications for Continuous-Time Signals." Theoretical Computer Science 410 (42): 4262–91. https://doi.org/10.1016/j.tcs.2009.06.021. ↩↩

  3. Donzé, Alexandre, and Oded Maler. 2010. "Robust Satisfaction of Temporal Logic over Real-Valued Signals." Formal Modeling and Analysis of Timed Systems (FORMATS 2010), 92–106. https://doi.org/10.1007/978-3-642-15297-9_9. ↩↩

  4. Annpureddy, Yashwanth, Che Liu, Georgios Fainekos, and Sriram Sankaranarayanan. 2011. "S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems." Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), 254–57. https://doi.org/10.1007/978-3-642-19835-9_21. ↩

  5. Ernst, Gidon, Paolo Arcaini, Georgios Fainekos, et al. 2021. "ARCH-COMP 2021 Category Report: Falsification with Validation of Results." 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), EPiC Series in Computing 80: 133–52. https://doi.org/10.29007/xwl1. ↩↩