Probabilistic Temporal Logic Falsification of Cyber-Physical Systems
- 1 May 2013
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Embedded Computing Systems
- Vol. 12 (2s), 1-30
- https://doi.org/10.1145/2465787.2465797
Abstract
We present a Monte-Carlo optimization technique for finding system behaviors that falsify a metric temporal logic (MTL) property. Our approach performs a random walk over the space of system inputs guided by a robustness metric defined by the MTL property. Robustness is guiding the search for a falsifying behavior by exploring trajectories with smaller robustness values. The resulting testing framework can be applied to a wide class of cyber-physical systems (CPS). We show through experiments on complex system models that using our framework can help automatically falsify properties with more consistency as compared to other means, such as uniform sampling.Keywords
Funding Information
- Division of Computer and Network Systems (CNS-1017074, CNS-1116136, CNS-1016994)
This publication has 36 references indexed in Scilit:
- Robustness of temporal logic specifications for continuous-time signalsTheoretical Computer Science, 2009
- Generalized Distance Functions in the Theory of ComputationThe Computer Journal, 2008
- An asynchronous integration and event detection algorithm for simulating multi-agent hybrid systemsACM Transactions on Modeling and Computer Simulation, 2004
- Generating test inputs for embedded control systemsIEEE Control Systems, 2003
- Hierarchical modeling and analysis of embedded systemsProceedings of the IEEE, 2003
- Dynamical properties of hybrid automataIEEE Transactions on Automatic Control, 2003
- What's Decidable about Hybrid Automata?Journal of Computer and System Sciences, 1998
- The algorithmic analysis of hybrid systemsTheoretical Computer Science, 1995
- Simulated annealing for constrained global optimizationJournal of Global Optimization, 1994
- Improving Hit-and-Run for global optimizationJournal of Global Optimization, 1993