Design and verification
Designing and verifying novel approaches to safety-centred software and hardware design.
Robotics and connected autonomous systems (RCAS) often need to work in challenging or inaccessible environments, such as nuclear facilities or at sea, and they need to adapt to changes in the environment.
To meet these challenges, we require rapid evolution of designs (including during operation), and the need for reconfiguration (both physical and logical) to remain effective.
If RCAS are designed without considering verification, it will not be possible to assure RCAS; a major emphasis of this pillar will be design for verification. This is both an issue for system architecture, and for the way algorithms are specified and designed. High levels of rigour are also needed in verification if RCAS are to be trusted in safety-critical applications.
- Developing adaptive approaches to RCAS control that are resilient in operation under extreme conditions.
- Developing techniques for the integration of software verification and validation for the design of integrated hardware and software systems in order that they can be assured.
- Developing integrated and compositional reasoning and testing over heterogeneous models.
- Automating verification techniques to ensure scalability.
Research Lead: Professor Ana Cavalcanti
Ana Cavalcanti is a Professor of Software Verification at the University of York and holds a ten-year Royal Academy of Engineering Chair in Emerging Technologies to work on Software Engineering for Robotics.
Previously, she held a Royal Society-Wolfson Research Merit Award, and a Royal Society Industry Fellowship to work with QinetiQ. Her research interest is the theory and practice of formal methods, with application to industry-strength techniques.