We are creating a sound theory for verification tools based on our coherent unifying mathematical framework (UTP). Unifying the relevant theories is the basis for a sound toolchain. We are building prototypes using our our dedicated verifier (Isabelle/UTP) to show feasibility of all our new tools and to link them to our existing tools. We are focusing on new features that have not been demonstrated before in any toolchain. We are building and exploiting models for model-based development, virtual verification and validation, prototyping, and the use of robotic digital twins. We are exploring new solutions for problems in two phases: an exploratory phase and an evaluation on case studies. We will generalise lessons from case studies to propose practical methods for engineers. All experiments and results will be publicly available for replication with curated tools and data.

We will provide a model-based framework for the cost-effective development of verifiably secure robots. This will provide ways to specify attacks and security properties. We will consider threats from the environment, other robots, or tampering with hardware and software. We will include libraries of threats and trusted architectures and techniques to deal with novel attacks. We will handle secure, reactive, timed, and hybrid properties.

We face socio-technical challenges: (1) Mobile and networked robots are sensitive to tampering. (2) Secure autonomy is often problematic interacting with humans. (3) Roboticists do not have a security culture. (4) Robotic systems need heterogeneous models under attack in a dynamic environment.