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

ABSTRACT

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.

REFERENCES

• 1: C. Bernardeschi, A. Fantechi, and S. Gnesi. Model checking fault tolerant systems. Software Testing, Verification and Reliability, 12(4):251--275, 2002.
• 2: Marco Bozzano , Adolfo Villafiorita, The FSAP/NuSMV-SA Safety Analysis Platform, International Journal on Software Tools for Technology Transfer (STTT), v.9 n.1, p.5-24, February 2007 [doi>10.1007/s10009-006-0001-2]
• 3: Glenn Bruns , Ian Sutherland, Model Checking and Fault Tolerance, Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology, p.45-59, December 13-17, 1997
• 4: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 5: Alessandro Cimatti, Industrial Applications of Model Checking, Proceedings of the 4th Summer School on Modeling and Verification of Parallel Processes, p.153-168, June 19-23, 2000
• 6: Alessandro Cimatti , Edmund M. Clarke , Fausto Giunchiglia , Marco Roveri, NUSMV: A New Symbolic Model Verifier, Proceedings of the 11th International Conference on Computer Aided Verification, p.495-499, July 06-10, 1999
• 7: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 8: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 9: Alan Fedoruk , Ralph Deters, Improving fault-tolerance by replicating agents, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy [doi>10.1145/544862.544917]
• 10: P. Gammie and R. van der Meyden. MCK: Model checking the logic of knowledge. In Proceedings of CAV'04, volume 3114 of LNCS, pages 479--483. Springer, 2004.
• 11: Z. Guessoum , J. P. Briot , S. Charpentier , O. Marin , P. Sens, A fault-tolerant multi-agent framework, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy [doi>10.1145/544862.544903]
• 12: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 13: R. Iyer. Experimental evaluation. In Proceedings of FTCS-25, pages 115--132. IEEE, 1995.
• 14: A. Joshi and M. P. E. Heimdahl. Model-based safety analysis of Simulink models using SCADE design verifier. In Proceedings of SAFECOMP'05, volume 3688 of LNCS, pages 122--135. Springer, 2005.
• 15: Alessio Lomuscio , Hongyang Qu , Marek Sergot , Monika Solanki, Verifying Temporal and Epistemic Properties of Web Service Compositions, Proceedings of the 5th international conference on Service-Oriented Computing, September 17-20, 2007, Vienna, Austria [doi>10.1007/978-3-540-74974-5_43]
• 16: Alessio Lomuscio , Hongyang Qu , Monika Solanki, Towards verifying compliance in agent-based web service compositions, Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems, May 12-16, 2008, Estoril, Portugal
• 17: A. Lomuscio and F. Raimondi. MCMAS: A model checker for multi-agent systems. In Proceedings of TACAS'06, volume 3920 of LNCS, pages 450--454. Springer, 2006.
• 18: A. Lomuscio and M. J. Sergot. Deontic interpreted systems. Studia Logica, 75(1):63--92, 2003.
• 19: A. Lomuscio and M. J. Sergot. A formalisation of violation, error recovery, and enforcement in the bit transmission problem. Journal of Applied Logic, 2(1):93--116, 2004.
• 20: A. Niewiadomski, W. Penczek, and M. Szreter. Verics 2004: A model checker for real time and multi-agent systems. In Proceedings of CS&P'04, Informatik-Berichte, pages 88--99, 2004.
• 21: Amir Pnueli, The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, p.46-57, September 30-October 31, 1977
• 22: M. J. Wooldridge. Reasoning about Rational Agents. MIT Press, Cambridge, 2000.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Verification

Keywords:
epistemic logic, fault injection, fault tolerance, model checking