Sciweavers

Share
ATAL
2009
Springer

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

9 years 6 months ago
Combining fault injection and model checking to verify fault tolerance in multi-agent systems
The ability to guarantee that a system will continue to operate correctly under degraded conditions is key to the success of adopting multi-agent systems (MAS) as a paradigm for designing complex agent based fault tolerant systems. In order to provide such a guarantee, practically usable tools and techniques for verifying fault tolerant MAS architectures are urgently required. In this paper we address this requirement by combining automatic fault injection with model checking to verify fault tolerance in MAS. We present a generic method to mutate a model of a correctly behaving system into a faulty one, and show how the mutated model can be used to reason about fault tolerance, which includes recovery from faults. The usefulness of the proposed method is demonstrated by injecting automatically a fault into a sender-receiver protocol, and verifying temporal and epistemic specifications of the protocol’s fault tolerance using the MCMAS model checker. Categories and Subject Descriptor...
Jonathan Ezekiel, Alessio Lomuscio
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where ATAL
Authors Jonathan Ezekiel, Alessio Lomuscio
Comments (0)
books