Automated analysis and verification of agent behavior

ABSTRACT

Comprehending and analyzing agent behavior is an arduous task due to complexities in agent systems and sophistication of agent behaviors, in addition to the common difficulties with any complex software system. This paper presents an integrated approach for the analysis and verification of behaviors of agent-based systems. The approach is a result of collaboration between the Tracer Tool and the TTL Checker, which together automate the analysis and verification of agents in an implemented agent system with the aim of aiding the user in redesigning, debugging, and maintaining the software system. The Tracer Tool ensures that the user's comprehension of the system behavior is accurate and provides explanations of anomalous behavior, which can be detected as a failed behavioral property by the TTL Checker. The integrated approach has been applied successfully in a case study in the domain of Unmanned Aerial Vehicles.

REFERENCES

• 1: Bosse, T., Jonker, C. M., Meij, L. van der, and Treur, J. A Temporal Trace Language for the Formal Analysis of Dynamic Properties. Technical Report, Vrije Universiteit Amsterdam, 2005.
• 2: Elliot J. Chikofsky , James H. Cross II, Reverse Engineering and Design Recovery: A Taxonomy, IEEE Software, v.7 n.1, p.13-17, January 1990 [doi>10.1109/52.43044]
• 3: Clarke, E. M., Grumberg, O., and Peled, D. A. Model checking. MIT Press, 2000.
• 4: Bruce Edmonds , Joanna J. Bryson, The Insufficiency of Formal Design Methods " The Necessity of an Experimental Approach - for the Understanding and Control of Complex MAS, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, p.938-945, July 19-23, 2004, New York, New York [doi>10.1109/AAMAS.2004.265]
• 5: P. J. Finnigan , R. C. Holt , I. Kalas , S. Kerr , K. Kontogiannis , H. A. Müller , J. Mylopoulos , S. G. Perelgut , M. Stanley , K. Wong, The software bookshelf, IBM Systems Journal, v.36 n.4, p.564-593, 1997
• 6: Garcia-Molina, H., Germano, F., and Kohler, W. Debugging a Distributed Computer System. IEEE Transactions on Software-Engineering, SE-10 (2), 1984, pp. 210--219.
• 7: D. N. Lam , K. S. Barber, Comprehending agent software, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands [doi>10.1145/1082473.1082562]
• 8: Lam, D. N. and Barber, K. S. Debugging Agent Behavior in an Implemented Agent System. In: Bordini, R. H., Dastani, M., Dix, J., Seghrouchni, A. E. F. (Eds.), Programming Multi-Agent Systems (Selected Revised and Invited Papers), Springer LNCS, vol. 3346, 2005, pp. 103--125.
• 9: Larsen, K. G., Petterson, P., and Yi, W. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1--2), 1997, pp. 134--152.
• 10: Divine T. Ndumu , Hyacinth S. Nwana , Lyndon C. Lee , Jaron C. Collis, Visualising and debugging distributed multi-agent systems, Proceedings of the third annual conference on Autonomous Agents, p.326-333, April 1999, Seattle, Washington, United States [doi>10.1145/301136.301220]

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Diagnostics; Monitors; Tracing; Debugging aids; Testing tools (e.g., data generators, coverage testing)

General Terms:
Documentation, Experimentation, Human Factors, Verification

Keywords:
agent-oriented software engineering, debugging, maintenance, reverse engineering, software comprehension, tracer, verification of agent systems