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.
展开▼
