We are developing a world-class, multi-disciplinary technical research programme to classify and relate verifiability concepts, notations, and techniques for autonomous systems. As part of this, we are designing algorithms and techniques to integrate verification across disciplinary domains.

Our current research direction is in developing theory, tools, and experiments in the application of sound and automated technology for the design and verification of secure robotic applications. The welcome growth of the robotics industry brings many new and risky challenges in cyber-security. As robots become connected and mobile, security becomes a central concern. Hacked robots are more sensitive than hacked computers because they perceive the real world. They are more dangerous because they change the real world. Cyber-security is an afterthought in implementing robots if considered at all. Some aspects must wait until implementation, such as covert channels in caches or buffer flushing, but it is difficult to articulate system security requirements at this late stage. This has a significant impact on cost and security. We are considering robot security right from the start.