Thursday, April 5, 2018
Speaker: Sergiy Bogomolov
Venue: IST Austria
A promising technique for the formal verification of
embedded and cyber-physical systems is flow-pipe construction, which
creates a sequence of regions covering all reachable states over time.
Flow-pipe construction methods can check whether specifications are
met for all states, rather than just testing using a finite and
incomplete set of simulation traces. A fundamental challenge when
using flow-pipe construction on high-dimensional systems is the cost
of geometric operations, such as intersection and convex hull. In this
talk, we address this challenge by showing that it is often possible
to remove the need to perform high-dimensional geometric operations by
combining two model transformations, direct time-triggered conversion
and dynamics scaling. Further, we discuss how to make the
overapproximation error in the conversion arbitrarily small. Finally,
we show that our transformation-based approach enables the analysis of
a drivetrain system with up to 51 dimensions.
Bio: Sergiy Bogomolov is on the faculty of the Australian National
University where he leads the Dependable Cyber Physical Systems Lab.
Prior to joining ANU Sergiy was a Postdoctoral Researcher in the
Institute of Science and Technology Austria. Sergiy is broadly
interested in algorithms and techniques to support design and
development workflow of trustworthy and resilient autonomous systems.
For this purpose, he uses and develops techniques on the interface of
cyber-physical systems verification and AI planning. His Ph.D. and
M.Sc. degrees are from the University of Freiburg, Germany.