Formal Verification of Merging Arbitration Control System for Logistics Robots
Nobuhiko MIYAMOTO, Hironobu Okamoto, Noriaki Ando, Yukikazu Koide · 2024
In this paper, we propose a traffic rule that can both improve the work efficiency of a logistics support robot performing picking work in a logistics center and avoid collisions at intersections, and describe the formal verification of a multiple AMR (Autonomous Mobile Robot) control system applying the proposed traffic rule using CSP (Communicating Sequential Processes) and time-expanded Timed-CSP. In a system where multiple AMRs are distributed and cooperate with each other, deadlock, which occurs when AMRs give way to each other, and livelock, which occurs when AMRs avoid each other, are problems. In this paper, we created a model of a multiple-AMR control system using CSP and Timed-CSP, which are effective formal methods for verifying concurrent systems, and verified it using the Process Analysis Toolkit (PAT). The validation results show that the Timed-CSP model of the proposed system does not cause deadlock or livelock, but there is a possibility of collision in the intersection when the CSP model is validated. Therefore, the verification results confirm that time-aware design is necessary for real-world systems.