Duration: 50:50

216 views

1

In this talk, we address the problem of falsifying properties of complex cyber-physical sytems that model the interactions between a discrete controller and a continuous physical environment. Often, such systems that are so complex that a symbolic approach to falsification is beyond the ability of existing solvers. We present two recent promising approaches to falsification based on the ideas of trajectory robustness and trajectory splicing. We show that the use of trajectory robustness can replace the standard Boolean interpretation of temporal logic properties with a real-valued interpretation that can guide the search for falsifying inputs. Furthermore, we present the idea of trajectory splicing that searches over multiple, possibly disconnected trajectory segments rather than a single trajectory. We present some promising results using our approach and discuss open challenges that will drive future research. Note: All relevant concepts will be explained during the talk. Joint work with Aditya Zutshi (U. Colorado Boulder), Georgios Fainekos (Arizona State University), Jyotirmoy Deshmukh and James Kapinski (Toyota Technical Center).