A Runtime Approach to Verify Scenario in Multi-agent Systems

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 multi-agent system. In this approach, scenarios are specified by Protocol Diagrams in AUML (Agent Unified Modeling Language), we formalize pre and post conditions of the scenarios and define an extension property class in JPF (Java Path Finder) 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.