Formal Modeling and Verification of Concurrent FSMs: Case Study on Event-Based Cooperative Transport Robots

Yoshinao ISOBE
Nobuhiko MIYAMOTO
Noriaki ANDO
Yutaka OIWA

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E104-D    No.10    pp.1515-1532
Publication Date: 2021/10/01
Publicized: 2021/07/08
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2020FOP0002
Type of Manuscript: Special Section PAPER (Special Section on Formal Approaches)
Category: 
Keyword: 
formal approach,  concurrent finite state machines,  process algebra,  model check,  cooperative robots,  robotic technology middleware,  

Full Text: PDF(4.4MB)>>
Buy this Article


Summary: 
In this paper, we demonstrate that a formal approach is effective for improving reliability of cooperative robot designs, where the control logics are expressed in concurrent FSMs (Finite State Machines), especially in accordance with the standard FSM4RTC (FSM for Robotic Technology Components), by a case study of cooperative transport robots. In the case study, FSMs are modeled in the formal specification language CSP (Communicating Sequential Processes) and checked by the model-checking tool FDR, where we show techniques for modeling and verification of cooperative robots implemented with the help of the RTM (Robotic Technology Middleware).

open access publishing via