Model-Aided Runtime Verification for Robotic Systems (MARVer) is a tool to formalize and automate the verification of the safety of robotic systems. MARVer is improved for the requirements and evaluation scenarios of UC11, which is an Automated robot inspection cell for quality control of the automotive body-in-white. And, the use-case owner is OTOKAR. The tool implements the improved method Model-Based Formal Specification and Verification For Robotic Systems (MBF). Robotic system developers generally appeal to design and implement robotic systems traditionally based on their expertise. The verification is implemented by trial and error. It is time-consuming, and it is not formal. MARVer is trying to facilitate the modeling of the systems, and it encourages the robotic systems developers to use modeling to verify the system; thus, it formalizes verification of the robotic system development. MARVer monitors and checks the safety requirements of the system during execution by taking the developer's task, and it reduces the workforce. The safety of robotic systems is not approved just by inspecting the system's software. The most critical safety issue in robotic systems is collision. Generally, the software of the robotic system does not provide data about the distances between the robot and obstacles. MARVer includes add-ons in order to get data like distances not provided by the system software.  

 MARVer is composed of three parts: MARVer-M, MARVer-R, and MARVer-S. MARVer-M is a system modeling and model checking tool based on UPPAAL It will facilitate the modeling process for the robotic systems. MARVer is the tool for runtime verification of robotic systems called Marver-R which is based on ROSMonitoring. It implements a meta-model in the background and provides a GUI to allow easy to configure and start runtime verification for ROS-compliant systems.