TY - JOUR AB - 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. AU - Ezekiel,J AU - Lomuscio,AR DO - 10.1016/j.ic.2016.10.007 EP - 194 PY - 2016/// SN - 1090-2651 SP - 167 TI - Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems T2 - Information and Computation UR - http://dx.doi.org/10.1016/j.ic.2016.10.007 UR - http://hdl.handle.net/10044/1/30096 VL - 254 ER -