Fault-Tolerance Verification in a Distributed Collective Collaborative Robotic System
Dakshinamurthy Sungeetha, Vasumathi K. Narayanan · 2014
In this paper, we model a collective collaborative robotic system which acts as a distributed system, solving the problem which a single robot cannot. A system consisting of n processes is modeled by a respective set of n communicating finite-state machines (CFSMs). Robotic processes often run concurrently and communicate with each other to accomplish a common goal. We begin from a specification of a set of robotic tasks in the form of CFSMs. As opposed to the traditional product automaton, built from a given specification of CFSMs, whose state-space explodes, we build a state-compressed model out of CFSMs. The model is composed by simulating the specified set of CFSMs in a global environment into a corresponding set of what are defined as communicating minimal prefix machines (CMPMs). The states of CMPMs form a well-founded, partial order. This model truly represents sequence, choice/non-determinism and concurrency exhibited by the concurrent robotic system tasks. The model provides a sound platform for performing state exploration/model-checking without exponential state explosion to verify both safety and liveness properties of the given set of robotic tasks.