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.
Case Study on Event-Based Cooperative Transport Robots
This work was supported by JSPS-KAKENHI Grant Number JP15H02687.
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:
- We show a formal development-process for cooperative robots with discrete dynamics as follows: design by concurrent FSM, formalization in CSP, verification by FDR, and implementation on RTM with FSM4RTC, as shown in Fig.1.
- We demonstrate how to formalize cooperative robots and verify them in detail, where some formal descriptions are generic and reusable for connecting RTCs and expressing requirements.
Figure 1 The formal development-process for cooperative robots
The detail of the case study is explained in the following paper:
- Yoshinao Isobe, Nobuhiko Miyamoto, Noriaki Ando, and Yutaka Oiwa, Formal Modeling and Verification of Concurrent FSMs: Case Study on Event-Based Cooperative Transport Robots, IEICE Transactions on Information and Systems, Vol.E104-D, No.10, pp.1515-1532 , October 2021. [ PDF (4.5MB) in J-STAGE ]
Video 1 Cooperative robots transporting a box
Video 2 Simulation for cooperative robots transporting a box
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
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
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
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
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
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.
-
The CSPM codes (i.e. CSP processes) for verifying
CoopSys can be downloaded.
CoopSys_CSP.zip (10KB) [MIT License] -
The following paper [ PDF (4.6MB) ]
can be downloaded from the website of
J-STAGE.
Formal Modeling and Verification of Concurrent FSMs: Case Study on Event-Based Cooperative Transport Robots, IEICE Transactions on Information and Systems, Vol.E104-D, No.10, pp.1515-1532 , October 2021.
Yoshinao Isobe
Cyber Physical Security Research Center
National Institute of Advanced Industrial Science and Technology (AIST), Japan
Cyber Physical Security Research Center
National Institute of Advanced Industrial Science and Technology (AIST), Japan