Robust Integrated Verification of Autonomous Systems
EPSRC grant no: EP/J01205X/1
RIVERAS aims to develop techniques and methodologies that can be used to design autonomous intelligent systems that are verifiably trustworthy. Research is focused:
- on developing flexible specifications that capture uncertainty and leave scope for self-adaptation of the system within a set of safety constraints.
- on developing V&V methods for state-of-the-art adaptive control algorithms.
Details of grant information can be viewed on the EPSRC website.
The RIVERAS team is led by Dr Kerstin Eder, Computer Science, who is an expert in Design Verification - the core focus of the research programme. The team includes Dr Arthur Richards from Aerospace Engineering who is an expert in optimisation and control for vehicle planning and decision making, and two experts in modelling vagueness and uncertainty in intelligent systems and formal specifications, Prof Jonathan Lawry and Prof Trevor Martin from Engineering Mathematics / Intelligent Systems Laboratory.
- Verification of high-level properties of control systems (stability, robustness) implemented in Simulink, using formal methods like theorem proving.
Demo of our proposed methodology and tool for translation from Simulink to Why3 language, applied to the verification of stability of a simple discrete system through eigenvalue analysis: