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:
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:
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
The CSPM codes (i.e. CSP processes) for verifying
CoopSys can be downloaded. CoopSys_CSP.zip
[MIT License]
