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.