This session is focused on practical techniques for the verification and validation of autonomous systems from specification via design to the code level. Because no single technique is adequate to cover a whole system in practice, a variety of verification techniques, including formal methods, such as model checking and theorem proving, and state-of-the-art simulation-based methods, will be presented from first principles and brought into the context of robotics. How these techniques can be applied will be illustrated using real-world examples. We will start with the verification of control system designs with respect to high-level requirements, such as stability, using an assertion-based approach that combines simulation-based verification with automatic theorem proving. We will then focus on using model-based techniques to enhance test generation in the context of coverage-driven verification applied to code used in robots that directly interact with humans. The session will finish with the proposal to design autonomous systems "for verification"; this requires a paradigm shift towards more systematic design practices.
The research presented in this session is based on collaborations within the EPSRC funded projects "Robust Integrated Verification of Autonomous Systems" and "Trustworthy Robotic Assistants". This session will be supplemented with hands-on demonstrations presented by Dejanira Araiza Illan.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599
