Automatic Verification of Multiagent Conversations
Abstract
As network bandwidth increases, distributed applications are becoming increasingly prevalent. Systems using these applications are very complicated to build and must be dependable. Software agents are ideal for breaking complicated problems into manageable subtasks. Agent conversations, a series of messages passed between agents, are the cornerstone of multiagent systems and must be deemed correct before being placed into service. This paper introduces a method to automatically verify that conversations are valid before employing them. Agent conversations are created graphically using state transition diagrams in the agentTool multiagent development environment. This graphical representation is then transformed into a formal modeling language called Promela that is analyzed by the Spin verification tool to detect errors such as deadlock, non-progress loops, syntax errors, unused messages, and unused states. Feedback is provided to the user automatically via text messages and graphical highlighting of error conditions.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2000
- Accession Number
- ADA446531
Entities
People
- Scott A. Deloach
- Timothy Lacey
Organizations
- Air Force Institute of Technology