Verifying Cross-Organizational Workflows Over Multi-Agent Based Environments

摘要

The agent oriented approach is increasingly used to provide flexible mechanisms for collaboration between cross-organizational processes. Most of research on this direction has been focused on agents that interact directly with partners hosted at specific locations. However, the design of a reliable model that integrates a multi-agent environment with a cross-organizational workflow becomes rather complex when mobility is considered. Few methods have been proposed advocating for the use of indirect protocols as the link between the environment and the workflows. Such protocols may couple heterogeneous agents and enforce their migration to specific locations in order to accomplish a collaboration. This paper presents a model based on nested Petri nets for achieving this integration. Besides, it explains how some properties of the overall system can be verified using the SPIN model checker.