Formal Analysis And Verification Of Agent-Oriented Supply-Chain Management

Managing various relationships among the supply chain processes is known as Supply Chain Management (SCM). SCM is the oversight of finance, information and material as they move in the flow from different suppliers to manufacturer, wholesaler, retailer and customers. The main problem with such software architecture is coordination and reliability while performing activities. Moreover, continuously changing market makes this coordination challenging. For example failure of production facilities, irregularities in meeting deadlines, unavailability of workers at required times. However, in the Agent-Oriented Supply-Chain Management described in [Mark S. Fox, Mihai Barbuceanu, and Rune Teigen "Agent-Oriented Supply-Chain Management". The International Journal of Flexible Manufacturing Systems, 12 (2000)] the proposed solution claims a remarkable coordination on the basis of an agent-oriented software architecture. In this paper, we formally specify architecture and verify it using model checking. We use UPPAAL to formally specify the agents' behaviour involved in SCM. By model-checking, we prove that the given SCM's architecture partially fulfills its functional requirements.