The software of autonomous robot systems is generally complex and safety critical. Therefore, formal specification and verification is a rather challenging task. Widely used testing and simulation alone are insufficient to ensure the correctness and safety of the system [MBF1, MBF2]. Although the software of robot systems is complex, fortunately, it can be designed as interacting but separate modules [MBF3]. Many people in the robotics research community use the robot operating system (ROS) which is a framework. Due to the modular structure of robot software, ROS allows the control of a robot to be carried out by functional modules operating as separate processes. A simple control scheme of a mobile robot system has multiple functional modules. Although the robotic inspection system (UC11) is targeted for verification, many industrial robot systems perform similar stages. Thus, the realization of the tasks performed by industrial robot systems takes place in a hierarchical series of stages. If the robot autonomy is increased, e.g., re-planning when the environment state changes and moving by feedback from the sensors that detect the environment during the movements, there may be a mutual flow between the stages and stages can become more complex. 

In the formal verification of robotic systems with model checking methods, the widely preferred and suitable model is timed automata [MBF5, MBF6]. Moreover, run-time verification methods are applied to robotics systems. Users provide formal safety and security specifications, and monitors are automatically generated and incorporated into the system to ensure the safety and security of robots [MBF7]. Model-checking, when combined with runtime verification, will improve the verification coverage and assurance on the operation of robotic systems [MBF4]. Verification methods to be used to verify the safety of robotic systems must comply with standards such as ISO 12100, IEC 61508, ISO 13849, ISO 10218-1, ISO 10218-2, ISO TS 15066 [MBF9, MBF10]. 

The method is implemented in two stages. In the first stage, once the requirements are given, the formal model of the robotic system is created. Then, by using the model-checking technique, the model is verified whether it meets the requirements or not. If not, the model is recursively revised until it meets all the requirements. In the second stage, the software of the robotic system is developed accordingly with the verified model. Then, the system software is subjected to runtime verification during execution integrating with the real system or a simulated environment.