The slides and the videos are available on eCampus.

Autonomous cars and unmanned aerial vehicles (UAV) are examples of autonomous systems, which can operate autonomously and interact with each other and with people in different (more or less) intelligent ways. They are characterised by the kind of interaction between the system and its environment and how they respond to changes in the environment. The design and deployment of autonomous systems, as for any other software system, must be done having in mind that the system satisfies certain functional and non-functional properties. One way to verify (and eventually guarantee) that the system is correct is by using formal methods.

Runtime Verification (RV)  is a formal methods technique that studies how to synthesise monitors from high-level formal specifications languages. RV focuses on the problem of observing a single execution trace, providing a formal framework for testing, debugging and monitoring, complementing other (static) verification techniques like model checking.

The objective of this seminar is to introduce RV in general and provide some examples of its use in the context of autonomous systems. For that, I will first give an overview of RV, and then show different scenarios where such technique can be used in the context of autonomous systems. At the end I will present challenges and interesting research directions in the domain.