|
Abstract:
|
Abstract: A scenario is a synthetic description of an event or series of actions and events. It plays an important role in software analysis and design, as well as verification and validation. In this paper, we propose an approach to verify the correctness of execution scenario in a multiagent system. In this approach, scenarios are specified by Protocol Diagrams in AUML (Agent Unified Modeling Language), we formalize pre and postconditions of the scenarios and define an extension property class in JPF (Java PathFinder) model checker to verify if the execution of scenarios satisfies their constraints. We use a well-known scenario of a book trading multi-agent system to illustrate our approach. © 2010 IEEE. |