Formal Modeling and Verification of Control Logic for Cooperative Robots

Yoshinao Isobe, Noriaki Ando, Nobuhiko MIYAMOTO, Geoffrey Biggs, Yutaka Oiwa · The Proceedings of JSME annual Conference on Robotics and Mechatronics (Robomec) · 2018

We present a formal approach for improving reliability of cooperative robot designs, where the control logics are expressed in FSMs (Finite State Machines), especially in accordance with the standard FSM4RTC (Finite State Machine for Robotic Technology Components). In our formal approach, FSMs are modeled in the formal specification language CSP (Communicating Sequential Processes) and checked by the model-checking tool FDR. Then, we demonstrate how the approach can be applied in the case study of cooperative transport robots.

Read the paper · More papers on PaperTik