Abstract

Cyber-physical systems (CPS) are networks of physical and digital components and present a next generation of large-scale highly-interconnected networked embedded systems. On the one hand, CPS open enormous opportunities as they form the core of emerging smart devices and services which are going to revolutionize many traditional industries such as automotive, traffic management, power generation and delivery, as well as manufacturing. On the other hand, highly autonomous systems pose special engineering challenges as any unexpected behaviour might lead to large financial losses or even human deaths.  In this talk, we address this challenge and propose automatic techniques to analyze CPS . For this purpose, we use the concept of hybrid automata which has proven to be particularly useful to model CPS .  Falsification algorithms for hybrid automata aim at finding trajectories that violate a given safety property. This is a challenging problem, and the practical applicability of current falsification algorithms still suffers from their high time complexity. In contrast to falsification, verification algorithms aim at providing guarantees that no such trajectories exist. Recent symbolic reachability techniques are capable of efficiently computing linear constraints that enclose all trajectories of the system with reasonable precision.  In this talk, we present an approach which leverages the power of symbolic reachability algorithms to improve the scalability of falsification techniques. Recent approaches to falsification reduce the problem to a nonlinear optimization problem. We propose to reduce the search space of the optimization problem by adding linear state constraints computed by a reachability algorithm. We showcase the efficiency of our approach on a number of standard hybrid systems benchmarks demonstrating the performance increase in speed and the number of falsifiable instances.