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

This work was supported by JSPS-KAKENHI Grant Number JP15H02687.

1. Introduction

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).

The contribution of this case study is summarized as follows:

Figure 1 The formal development-process for cooperative robots

The detail of the case study is explained in the following paper: In this web-site, we give demonstrative videos of the cooperative transport robots, and briefly introduce the case study. Videos 1 and 2 show demonstrations of the cooperative robots developed in accordance with the formal development-process introduced above, where Raspberry-Pi Mouse (hardware) is used as a transportation robot in Video 1 and a simulator (software) is used for the robots and the environment in Video 2.

Video 1 Cooperative robots transporting a box

Video 2 Simulation for cooperative robots transporting a box

2. An Example: Cooperative Transport Robots

A cooperative robot system, named CoopSys , is used for a case study. As shown in the top of Fig.2, the cooperative robot system consists of two cooperative robots CoopRobo(1),(2) , two home bases (charging stations) Home1,2 , the goal location Goal , and an object box Box . The two robots cooperatively transport the box to the goal location, where each robot has a rechargeable battery and can charge on its home base.Here, it is important that sole transportation is forbidden for the safety. Figure 2 also shows a basic scenario for cooperatively transporting Box to Goal.

Figure 2 A basic scenario of cooperative transportation in CoopSys

A part of state-transitions in the system-level caused by mode-changes of the two cooperative transport robots is shown in Fig.3.

Figure 3 A part of state-transitions in CoopSys

3. Design in Concurrent FSMs

We design the structure of the cooperative robot system CoopSys on the assumption that it is implemented on RTM (RT-Middleware), which is a software platform for autonomous RTCs (RT-Components), thus CoopSys is a system concurrently composed of RTCs. The structure of CoopSys is shown in Fig.4, where each box represents an RTC and each connection rep- resents an event passing between RTCs.

Figure 4 The structure (RTCs and connections) of CoopSys

The control logic of each RTC in Fig.4 is expressed by a finite state machine (FSM). For example, the FSMs, named RoboMng and RoboCtrl, of the RTC RoboMngRTC and RoboCtrlRTC are shown in Figs.5 and 6, respectively. The FSMs have the two-level hierarchy. The five top-level states in Fig.5, Approach, Ready, Transport, Return, and Charge, correspond to the five control-modes in CoopRobo(i), and the top-level state Return Charge is the common part of Return and Charge because the responses to events in the two modes are similar.

Figure 5 The finite state machine RoboMng of the RTC RoboMngRTC

Figure 6 The finite state machine RoboCtrl of the RTC RoboCtrlRTC

4. Formalization in CSP

We formally express the design of the cooperative robot system CoopSys in CSP (Communicating Sequential Processes), which is one of well known formal description languages for expressing concurrent behaviors. For example, the CSP process (formal description) corresponding to the FSM RoboMng in Fig.5 is shown in Fig.7.

Figure 7 The CSP-process of the FSM RoboMng

5. Verification by FDR

The model checker FDR (Failures-Divergences Refinement) is a tool for exhaustively checking the behavior of CSP-processes written in CSPM (Machine-readable CSP), where CSPM is the formal specification language combining the operators of CSP with a functional language. Figure 8 shows the result of the verification for the cooperative robot system CoopSys and the "Finished: Failed" in "SafeSpec [T= CoopSys" means that that sole transportation is possible in CoopSys.

Figure 8 The results of model-checking by FDR

By clicking the button "Debug" in Fig.8, a counter-example for the sole transportation is displayed in the debugger as shown in the left side of Fig.9. The counter-example is a critical trace, whose length is 192, leading to the sole transportation. The critical trace can be analyzed by decomposing it to component-wise partial traces. For example, the partial trace related to RoboMng(2) included in the critical trace is displayed in the right pane of the debugger in Fig.9. The two abstract partial traces related to RoboMng(1) and RoboMng(2) extracted from the critical trace are shown in the right side of Fig.9. The interaction of the two abstract partial traces shows that the sole transportation is caused by the almost simultaneous occurrence of the two output-events out.ready and out.cancel. In this case, CoopRobo(2) solely transports a box because the ready-flag rdy remains True after receiving the event ready. The critical trace can be removed by adding the output-event out.cancel on the two transitions from the substates Select in the two states Ready and Transport to the state Return in the FSM RoboMng in Fig.5.

Figure 9 The debugger for analyzing a trace to sole transportation and the two extracted sub-traces

6. Implementation on RTM with help of FSM4RTC

RTM is a software platform standard in OMG (Object Management Group) for constructing robot systems by hierarchically connecting RT-Components (RTCs), and OpenRTM-aist is an implementation of RTM. FSM4RTC is an extended-standard of RTC in OMG for supporting implementation of FSMs in RTCs, and is implemented as a library of RTM. We implemented the FSMs such as RoboMng and RoboCtrl in RTCs with help of FSM4RTC. Then, we connected the RTCs by a tool RTCBuilder, which provides a graphical editor as shown in Fig.10.

Figure 10 The graphical connections between RTCs by the RTCBuilder

7. Conclusion

We formalized cooperative transportation robots with FSMs in the specification language CSP and verified the correctness of the behavior by the model checker FDR, where some abstractions of the behavior are applied as explained in Sect. 3.2 to avoid state-space explosion. In this case study, we found several design-errors by FDR. It is hard to detect such design-errors by testing the implementation of the design because failures caused by the errors are rarely observed. It is still costly to formalize and verify cooperative systems, but it is useful for detecting design-errors of cooperative systems, which contain non-deterministic behaviors, and can reduce the costs for implementation and testing.

8. Download

9. Contact

Yoshinao Isobe
Cyber Physical Security Research Center
National Institute of Advanced Industrial Science and Technology (AIST), Japan

Last modified: 5 October 2021

(since 27/09/2021)