An Automated Approach to Verifying Diagnosability in Multi-agent Systems

—This paper addresses the issue of guaranteeing the correctness of fault diagnosis mechanisms in multi-agent systems. We propose an automated approach to verifying the property of diagnosability by combining fault injection with model checking. In particular we show how to reason about individual agent’s and system wide knowledge of faults, which is essential for the agents to cooperate and coordinate to recover from them. The multiagent system model checker MCMAS is used for verification and epistemic specifications are defined to specify that a system accurately diagnoses faults.

• Type: Conference
• Year: 2009
• Where: SEFM
• Authors: Jonathan Ezekiel, Alessio Lomuscio
• Keywords: Fault Diagnosis Mechanisms, Fault Injection, Model Checker Mcmas, SEFM 2009, Software Engineering