Verification of Agent Behavioral Models

Intelligent software agents are becoming very popular. They are ideal for solving distributed problems that are too difficult for a non-distributed system to solve. Distributed agents can be used to retrieve, filter, and summarize information as well as provide intelligent user interfaces. However, multiagent systems are very complicated to build and must be dependable. Agent conversation protocols, a series of messages passed between agents, are the cornerstone of multiagent systems. Agents also have tasks associated with them that specify how an agent behaves. This paper introduces a formal methodology that automatically verifies the interaction between agents. Agent behavioral specifications are created graphically in the agentTool multiagent development environment. This graphical representation is then transformed into a formal modeling language called Promela that is analyzed by Spin to ensure the interaction between agents is correct. This type of verification provides the user with another tool to ensure the system will perform as expected.