Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems

We present an automated technique that combines fault injection with model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems. We define a general method for mutating a multi-agent systems model representing correct behaviour by injecting faults into it, and specification patterns based on temporal-epistemic formulas to reason about the correct and faulty behaviours of the mutated model. The technique is implemented in a toolkit that can be used for injecting automatically faults into a multi-agent systems program. The usefulness of the methodology is demonstrated by injecting a number of faults into a model of the IEEE 802.5 token ring LAN protocol and analysing the protocol's fault tolerance, by verifying a number of temporal-epistemic specifications.