Trusted Autonomous Systems: Verification Meets Falsification

Add to your list(s) Download to your calendar using vCal

• Sergiy Bogomolov
• Wednesday 27 July 2022, 14:00-14:30
• Discussion Room, Newton Institute.

If you have a question about this talk, please contact nobody.

VSO2 - Verified software

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. 

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Discussion Room, Newton Institute
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• bld31

Note that ex-directory lists are not shown.