HTP Graphics

LEAD RESEARCHER: ANGELO FERRANDO I am a Postdoctoral Research Associate at the University of Manchester since July 2020. I am part of the Autonomy and Verification Network, where I work on applying Runtime Verification (RV) in the RAIN Hub. Previously, I was a Research Associate at the University of Liverpool from 2018 to 2020. My main research interests are Formal Methods, Software Engineering, Multi-Agent Systems and Runtime Verification; the latter especially when applied to improve the reliability of intelligent systems. I am a member of the program committee in several international conferences such as PRIMA, AAMAS and CAI. RUNTIME VERIFICATION SUMMARY // Cyber-physical systems are complex; both from a design and implementation perspective. When applied in safety-critical scenarios, it is crucial to be confident nothing wrong is going to happen. Formal Verification is a research area whose aim is to increase the reliability of systems, by analysing their behaviour before deployment (static), of after deployment (dynamic). Runtime Verification is a verification technique which uses monitors to control the system execution. These monitors check the system against the expected behaviour and allow it to intervene in case of unexpected events. This technique is well suited to be used in robotics, since robotic applications are generally hard to model, and monitors can give an additional layer of trust. We designed and developed a Runtime Verification framework, called ROSMonitoring, to verify at runtime ROS-based robotic applications. We applied this framework in many different scenarios, and we showed how monitoring helped improving system robustness. 24 "RUNTIME VERIFICATION IS A VERIFICATION TECHNIQUE WHICH USES MONITORS TO CONTROL THE SYSTEM EXECUTION. THESE MONITORS CHECK THE SYSTEM AGAINST THE EXPECTED BEHAVIOUR AND ALLOW IT TO INTERVENE IN CASE OF UNEXPECTED EVENTS. "

• Cover