Issue link: https://htpgraphics.uberflip.com/i/1385717
LEAD RESEARCHER: RAFAEL C. CARDOSO I am a Postdoctoral Research Associate at the University of Manchester. I am part of the Autonomy and Verification Network, where I work in the research hubs RAIN and FAIR-SPACE. My main research themes include combining multi-agent systems with multi-agent planning, and integrating formal verification in software development. RAIN has provided me with several realistic case studies that have been fundamental in the evaluation of the techniques I have worked on for the autonomy and verification of modular robotic systems. SUMMARY // Autonomous robotic systems can be hard to formally verify. It is important to be able to separate the autonomous decision-making from the low-level control of the robot, thus allowing the core intelligence of the robot to be more amenable to formal verification, a process that can be time consuming and sometimes intractable for large systems. These systems are increasingly often modular, which favour the use of compositional verification approaches. We tackle these problems through two different contributions. First, we created an interface (ROS-A) for using cognitive agents in the high-level autonomous decision-making of the robot to isolate the core intelligence to a more compact representation that can be formally verified using a model checker (exhaustive exploration of the search space). Second, we have developed a compositional approach that allows us to specify First-Order Logic (FOL) contracts for each individual component and then apply some inference rules to derive system-level properties. AUTONOMY AND VERIFICATION OF MODULAR ROBOTIC SYSTEMS 26