Deploying safe and dependable cyber-physical systems requires one to verify their behaviours against formal specifications. The physical aspect of such systems by virtue of them being embedded in a continuous universe generate continuous-time signals. This leads to the main question of interest and the focus of this talk. When does a continuous-time signal satisfy a formal specification? Answering this question is harder than it might first appear, because an uncountably infinite number of points must be tested.Since the outcome of the test is boolean, continuity does not come readily to our aid. A naive sampling strategy can offer no guarantees about what happens between sampling instants. A computational solution for arbitrary signals is therefore impossible. But is there a class of signals for which more can be said? We demonstrate that polynomials (and more generally, polynomial splines) can be verified exactly without any loss of information, and present a new algorithm for doing so.

Iman Shames is currently a Professor of Mechatronics at the School of Engineering at the Australian National University. Previously, he had been an Associate Professor at the Department of Electrical and Electronic Engineering, the University of Melbourne from 2014 to 2020 and a Senior Lecturer and a McKenzie fellow at the same department from 2012 to 2014, and before that he was an ACCESS Postdoctoral Researcher at the ACCESS Linnaeus Centre, the KTH Royal Institute of Technology, Stockholm, Sweden. He received his B.Sc. degree in Electrical Engineering from Shiraz University in 2006, and the Ph.D. degree in engineering and computer science from the Australian National University, Canberra, Australia in 2011. His current research interests include, but are not limited to, optimization theory and its application in control and estimation, mathematical systems theory, and security and privacy in cyber–physical systems.