Issue link: https://htpgraphics.uberflip.com/i/1385717
VERIFICATION & VALIDATION RAIN PROGRESS // The ROS-A interface for programming verifiable autonomous agents in ROS is available at https://github. c o m /a u to n o my- a n d -ve r i f i c a t i o n - u o l /g we n d o l e n - rosbridge. It has been used in 3D simulations of various robots, such as Jackal, Husky, Mars Curiosity rover, and TurtleBot 2 and 3. With this interface, agents can publish messages (such as commands to actuators) to a ROS topic or can subscribe to a topic to receive messages (such as perceptions from sensors). Our tools for compositional verification include a ROS Contract Language (RCL) and a parsing tool called Vanda, both are available at https://github.com/autonomy-and- verification/ros-contract-language. RCL is a domain- specific language for describing the FOL contracts and linking each contract to the topic information from its respective ROS node. Vanda is a parsing tool that automatically synthesises ROS monitors from RCL descriptions. The ROS monitors are generated into ROSMonitoring, a tool that we have developed for runtime verification of ROS-based systems, which is available at https://github.com/autonomy-and-verification-uol/ ROSMonitoring. Verifying that modular robotic systems behave as expected requires verification methods that can cope with, and preferably take advantage of, their inherent modularity. FUTURE ASPIRATIONS // Opportunities for future collaboration include the use of our publicly available tools and providing feedback so that we can fix any reported problems and extend the tools with new feature requests. Applying our approaches to new and complex industrial use cases can further improve them and potentially open new research problems to be solved. We have been collaborating with the National Institute of Standards and Technology (NIST) in the US to make an agent interface for their Canonical Robot Command Language, a lightweight, modular component where messages provide robot motion and control with grasping as an abstraction. For the interface, it would be useful to have field experiments with several robots to test the added delay (if any) when compared to traditional control code in C++ and Python, and to test the integration of multi-robot scenarios using the interface. For the compositional verification approach, we also intend to explore the use of the FOL contracts to guide the heterogeneous verification of each individual component using the verification technique/tool most appropriate for the job. UNIQUENESS // By adding verifiable cognitive agents to perform high-level decision making we can improve usability, modularity, and reliability of the robotic system. Our interface for programming these agents works directly with many versions of the Robot Operating System (ROS), a popular middleware in the development of robots. Our compositional verification approach is not only capable of specifying contracts and system-level properties for modular robotic systems, but can also automatically translate these contracts into ROS monitors that can act as a safety net, verifying the contracts at runtime. 27